Monad7 = HOL_Gen + Monad + rules ax1 "mapM id = id" ax2s "mapM f o mapM g = mapM (f o g)" ax3s "unitM o f = mapM f o unitM" ax4 "joinM o mapM (mapM f) = mapM f o joinM" ax5 "joinM o unitM = id" ax6 "joinM o mapM unitM = id" ax7 "joinM o mapM joinM = joinM o joinM" defs ax8 "extM f == joinM o mapM f" E6 "(g oM f) == extM g o f" end