Changeset 1648 for src/utilities
- Timestamp:
- Jan 18, 2012, 11:01:14 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/utilities/monad.ma
r1647 r1648 126 126 interpretation "monad sigbind2" 'm_sigbind2 m f = (m_sigbind2 ????? m f). 127 127 128 (* 128 129 check (λM : Monad.λA,B,C,P.λp.λf : ∀a,b.P 〈a,b〉 → monad M C.! «a,b,H» ← p; f a b H) 130 *) 129 131 130 132 record MonadProps : Type[1] ≝
Note: See TracChangeset
for help on using the changeset viewer.