sync

Stdlib/Data/Applicative.juvix

@@ -9,7 +9,9 @@ type Applicative (f : Type -> Type) :=
     functor : Functor f;
     pure : {A : Type} -> A -> f A;
     syntax operator <*> lapp;
+    -- use apply and define <*>
     <*> : {A B : Type} -> f (A -> B) -> f A -> f B;
+    -- app
   };
 
 open Applicative public;

Stdlib/Data/Functor.juvix

@@ -7,6 +7,7 @@ trait
 type Functor (f : Type -> Type) :=
   mkFunctor {
   -- TODO what about calling it map? (like in Lean)
+  -- YES
     fmap : {A B : Type} -> (A -> B) -> f A -> f B
   };
 

Stdlib/Data/Monad.juvix

@@ -9,6 +9,7 @@ type Monad (f : Type -> Type) :=
   mkMonad {
     applicative : Applicative f;
     syntax operator >>= seq;
+    -- bind
     >>= : {A B : Type} -> f A -> (A -> f B) -> f B;
   };