Skip to content

Commit

Permalink
update stdlib
Browse files Browse the repository at this point in the history
  • Loading branch information
janmasrovira committed Feb 26, 2025
1 parent 7c49ce7 commit de840b5
Show file tree
Hide file tree
Showing 2 changed files with 7 additions and 7 deletions.
2 changes: 1 addition & 1 deletion juvix-stdlib
12 changes: 6 additions & 6 deletions tests/Compilation/positive/test091.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@ StateT-Functor
instance
StateT-Applicative
{S : Type} {M : Type -> Type} {{Monad M}} : Applicative (StateT S M) :=
mkApplicative@{
Applicative.mk@{
ap {A B} : StateT S M (A -> B) -> StateT S M A -> StateT S M B
| (mkStateT mf) (mkStateT mx) :=
mkStateT
Expand All @@ -77,7 +77,7 @@ StateT-Applicative
instance
StateT-Monad
{S : Type} {M : Type → Type} {{mon : Monad M}} : Monad (StateT S M) :=
mkMonad@{
Monad.mk@{
applicative := StateT-Applicative;
bind
{A B : Type} (x : StateT S M A) (f : A → StateT S M B) : StateT S M B :=
Expand Down Expand Up @@ -152,7 +152,7 @@ ReaderT-Applicative
{M : Type → Type}
{{func : Applicative M}}
: Applicative (ReaderT S M) :=
mkApplicative@{
Applicative.mk@{
pure {A} (a : A) : ReaderT S M A := mkReaderT λ{s := Applicative.pure a};
ap {A B} : ReaderT S M (A -> B) -> ReaderT S M A -> ReaderT S M B
| (mkReaderT mf) (mkReaderT ma) :=
Expand All @@ -162,7 +162,7 @@ ReaderT-Applicative
instance
ReaderT-Monad
{S : Type} {M : Type → Type} {{mon : Monad M}} : Monad (ReaderT S M) :=
mkMonad@{
Monad.mk@{
applicative := ReaderT-Applicative;
bind
{A B : Type}
Expand Down Expand Up @@ -229,15 +229,15 @@ Identity-Functor : Functor Identity :=

instance
Identity-Applicative : Applicative Identity :=
mkApplicative@{
Applicative.mk@{
pure := mkIdentity;
ap {A B} : Identity (A -> B) -> Identity A -> Identity B
| (mkIdentity f) (mkIdentity x) := mkIdentity (f x);
};

instance
Identity-Monad : Monad Identity :=
mkMonad@{
Monad.mk@{
bind {A B : Type} : Identity A -> (A -> Identity B) -> Identity B
| (mkIdentity a) f := f a;
};
Expand Down

0 comments on commit de840b5

Please sign in to comment.