Skip to content

Commit

Permalink
Merge pull request #958 from JasonGross/coq-8.16+better-monad-errors
Browse files Browse the repository at this point in the history
Add bidi type inference to monad class constructors
  • Loading branch information
mattam82 authored Mar 15, 2024
2 parents 3704614 + a200254 commit 969790e
Showing 1 changed file with 2 additions and 0 deletions.
2 changes: 2 additions & 0 deletions utils/theories/monad_utils.v
Original file line number Diff line number Diff line change
Expand Up @@ -12,11 +12,13 @@ Class Monad@{d c} (m : Type@{d} -> Type@{c}) : Type :=
{ ret : forall {t : Type@{d}}, t -> m t
; bind : forall {t u : Type@{d}}, m t -> (t -> m u) -> m u
}.
Global Arguments Build_Monad _ & _ _. (* for better type inference and error messages *)

Class MonadExc E (m : Type -> Type) : Type :=
{ raise : forall {T}, E -> m T
; catch : forall {T}, m T -> (E -> m T) -> m T
}.
Global Arguments Build_MonadExc _ _ & _ _. (* for better type inference and error messages *)


Module MCMonadNotation.
Expand Down

0 comments on commit 969790e

Please sign in to comment.