Skip to content

Commit c0c934c

Browse files
authored
Merge pull request #60 from Lysxia/implicit-arg-monads
Implicit arguments for mkOptionT, mkEitherT, mkIdentT
2 parents ca87e9e + cf6b3a4 commit c0c934c

File tree

3 files changed

+10
-1
lines changed

3 files changed

+10
-1
lines changed

theories/Data/Monads/EitherMonad.v

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -104,3 +104,6 @@ Section except.
104104
}.
105105

106106
End except.
107+
108+
Arguments mkEitherT {T} {m} {A} (_).
109+
Arguments unEitherT {T} {m} {A} (_).

theories/Data/Monads/IdentityMonad.v

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,4 +11,7 @@ Section Ident.
1111
; bind := fun _ _ c f => f (unIdent c)
1212
}.
1313

14-
End Ident.
14+
End Ident.
15+
16+
Arguments mkIdent {A} (_).
17+
Arguments unIdent {A} (_).

theories/Data/Monads/OptionMonad.v

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -99,3 +99,6 @@ Section Trans.
9999
}.
100100

101101
End Trans.
102+
103+
Arguments mkOptionT {m} {a} (_).
104+
Arguments unOptionT {m} {a} (_).

0 commit comments

Comments
 (0)