Commits

Anonymous committed 1068673 Draft

.

Comments (0)

Files changed (3)

 
   Definition test1 (lst : list nat) : res myerr (list nat) :=
     if eq_dec lst nil
-    then throw Empty
+    then throw Empty (M := Identity)
     else
       h <- test1_aux lst;;
       ret $ h :: lst
   Eval compute in test1 (1 :: 0 :: 3 :: nil).
   Eval compute in test1 nil.
 
-
-(*
-Typeclasses eauto := debug bfs.
-*)
 Check test1.
 
-  Definition test2 (* : resT _ (State bool) *)
+
+Typeclasses eauto := debug bfs.
+
+  Definition test2
+ : resT myerr (@StateT_Monad_inst bool identity_type Identity) (list nat)
    :=
-    lift (t := stateT bool) (put true);;
-    r <- catch
+    lift $ (put true);;
+    r <-
       (catch
         (test1 nil)
         (fun e =>
 Class MonadTrans
   {m : Type -> Type}
   {M : Monad m}
-  (t : forall {m} (M : Monad m), Type -> Type)
+  (t : forall m (M : Monad m), Type -> Type)
   {TM : Monad (t m M)} :=
 { lift : forall {A}, m A -> t m M A
 ; MonadT0 : forall A,
 (S : Type)
 {m : Type -> Type}
 (M : Monad m)
-`{ Monad (stateT S m) }
 :=
   { get : stateT S m S
   ; put : S -> stateT S m unit
    |}
 .
 
-
-
-Instance State_monadT_inst
-  S
-  {m}
-  {M : Monad m}
-:
-  MonadTrans (stateT S)
+Instance State_monadT_inst S
+{m} {M : Monad m}
+: @MonadTrans m M (@stateT S) (StateT_Monad_inst S m)
 :=
-  { lift := fun A (v : m A) =>
+  { lift := fun {A} (v : m A) =>
       fun s =>
         a <- v ;;
         ret (a, s)
   }
 .
 (* T0 *)
-intros.
+intros; simpl.
 extensionality x.
 extensionality y.
 rewrite Monad0.
 reflexivity.
 (* T1 *)
 intros. simpl.
-
 extensionality q.
-
-Lemma bindpair : forall A S R m (M : Monad m) (f : A -> S -> m R)
-  (v : m A) (s : S),
-  (ma <- (a <- v ;; ret (a, s)) ;;
-   let (ma_r, ma_s) := ma in f ma_r ma_s
-  )
-  =
-  (a <- v ;; f a s
-  ).
-intros.
-rewrite Monad2.
+repeat rewrite Monad2.
 f_equal.
-extensionality q.
-rewrite Monad0.
-reflexivity.
-Qed.
-
-rewrite -> bindpair.
-rewrite Monad2.
+extensionality r.
+repeat rewrite Monad0.
 reflexivity.
 Defined.
 
 Eval compute in evalState test1 true.
 
 End Examples.
-
-
-
-
-
-
-
-
-
-
-