Changeset 1648 for src/utilities

Timestamp:

Jan 18, 2012, 11:01:14 AM (9 years ago)

Author:

mulligan

Message:

new version of utilities/monad.ma with typecheck command comented out

File:

• src/utilities/monad.ma (modified) (1 diff)

src/utilities/monad.ma

@@ -126 +126 @@
 interpretation "monad sigbind2" 'm_sigbind2 m f = (m_sigbind2 ????? m f).
 
+(*
 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)
+*)
 
 record MonadProps : Type[1] ≝