Freer Monad in Lean

Stream: new members

[Simon Daniel]

im Trying to implement a Freer Monad that describes a Sequence of Effects.
One Effect E however should be allowed to contain such a Effect sequence itself (e.g. to branch between two continuations)

inductive Freer (Eff:Type u → Type v) (α:Type w) where
| Do: Eff β → (β → Freer Eff α) → Freer Eff α
| Return: α → Freer Eff α

inductive E (α:Type) where
| e:  (Bool -> Freer E α)  -> E α -- branches the Effect Sequence

ive seen this in a Haskell code example and wondered if this works in Lean aswell

[Notification Bot]

A message was moved here from #new members > universe levels by Simon Daniel.