source
@[instance 100]
instance Lake.instAlternativeOfMonadOfMonadExceptOfPUnit_lake {m : Type u_1 → Type u_2} [Monad m] [MonadExceptOf PUnit m] :
Alternative m
Equations

- Lake.instAlternativeOfMonadOfMonadExceptOfPUnit_lake = { toApplicative := inst✝¹.toApplicative, failure := fun {α : Type ?u.18} => throw (), orElse := fun {α : Type ?u.18} => tryCatch }

source
@[instance 10000]
instance Lake.instMonadLiftTOfMonadLift_lake {α : Type u_1 → Type u_2} {β : Type u_1 → Type u_3} [MonadLift α β] :
MonadLiftT α β

Ensure direct lifts are preferred over indirect ones.

Equations

- Lake.instMonadLiftTOfMonadLift_lake = { monadLift := fun {α_1 : Type ?u.19} => MonadLift.monadLift }

source
@[instance 100]
instance Lake.instMonadLiftTIdOfPure_lake {m : Type u_1 → Type u_2} [Pure m] :
MonadLiftT Id m
Equations

- Lake.instMonadLiftTIdOfPure_lake = { monadLift := fun {α : Type ?u.15} (act : Id α) => pure act.run }

source
@[instance 100]
instance Lake.instMonadLiftTOptionOfAlternative_lake {m : Type u_1 → Type u_2} [Alternative m] :
MonadLiftT Option m
Equations

- Lake.instMonadLiftTOptionOfAlternative_lake = { monadLift := fun {α : Type ?u.18} (x : Option α) => match x with | some a => pure a | none => failure }

source
@[instance 100]
instance Lake.instMonadLiftTExceptOfPureOfMonadExceptOf_lake {m : Type u_1 → Type u_2} {ε : Type u_3} [Pure m] [MonadExceptOf ε m] :
MonadLiftT (Except ε) m
Equations

- One or more equations did not get rendered due to their size.

source
@[instance 100]
instance Lake.instMonadLiftTReaderTOfBindOfMonadReaderOf_lake {m : Type u_1 → Type u_2} {ρ : Type u_1} {n : Type u_1 → Type u_3} [Bind m] [MonadReaderOf ρ m] [MonadLiftT n m] :
MonadLiftT (ReaderT ρ n) m
Equations

- Lake.instMonadLiftTReaderTOfBindOfMonadReaderOf_lake = { monadLift := fun {α : Type ?u.34} (act : ReaderT ρ n α) => do let __do_lift ← read liftM (act __do_lift) }

source
@[instance 100]
instance Lake.instMonadLiftTStateTOfMonadOfMonadStateOf_lake {m : Type u_1 → Type u_2} {σ : Type u_1} {n : Type u_1 → Type u_3} [Monad m] [MonadStateOf σ m] [MonadLiftT n m] :
MonadLiftT (StateT σ n) m
Equations

- One or more equations did not get rendered due to their size.

source
@[instance 100]
instance Lake.instMonadLiftTOptionTOfMonadOfAlternative_lake {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [Monad m] [Alternative m] [MonadLiftT n m] :
MonadLiftT (OptionT n) m
Equations

- Lake.instMonadLiftTOptionTOfMonadOfAlternative_lake = { monadLift := fun {α : Type ?u.29} (act : OptionT n α) => liftM act.run >>= liftM }

source
@[instance 100]
instance Lake.instMonadLiftTExceptTOfMonadOfMonadExceptOf_lake {m : Type u_1 → Type u_2} {ε : Type u_1} {n : Type u_1 → Type u_3} [Monad m] [MonadExceptOf ε m] [MonadLiftT n m] :
MonadLiftT (ExceptT ε n) m
Equations

- Lake.instMonadLiftTExceptTOfMonadOfMonadExceptOf_lake = { monadLift := fun {α : Type ?u.33} (act : ExceptT ε n α) => liftM act.run >>= liftM }

source
@[instance 100]
instance Lake.instMonadLiftTEIOOfMonadOfMonadExceptOfOfBaseIO_lake {m : Type → Type u_1} {ε : Type} [Monad m] [MonadExceptOf ε m] [MonadLiftT BaseIO m] :
MonadLiftT (EIO ε) m
Equations

- Lake.instMonadLiftTEIOOfMonadOfMonadExceptOfOfBaseIO_lake = { monadLift := fun {α : Type} (act : EIO ε α) => liftM act.toBaseIO >>= liftM }