inductive EffectKind : Type

• pure: EffectKind
• impure: EffectKind

instance instReprEffectKind : Repr EffectKind

Equations

• instReprEffectKind = { reprPrec := reprEffectKind✝ }

instance instDecidableEqEffectKind : DecidableEq EffectKind

Equations

• instDecidableEqEffectKind x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯

@[reducible]

def EffectKind.toMonad (e : EffectKind) (m : Type → Type) : Type → Type

Equations

• EffectKind.pure.toMonad m = Id
• EffectKind.impure.toMonad m = m

@[simp]

theorem EffectKind.toMonad_pure {m : Type → Type} : EffectKind.pure.toMonad m = Id

@[simp]

theorem EffectKind.toMonad_impure {m : Type → Type} : EffectKind.impure.toMonad m = m

NOTE: The Monad instance below also implies Functor, Applicative, etc. If m is a Functor, but not a full Monad, then e.toMonad m should still be a functor too. However, actually having these instances causes diamond problems with the aforementioned instances implied by Monad. Thus, we just assume m is always a monad.

instance EffectKind.instMonadToMonad {e : EffectKind} {m : Type → Type} [Monad m] : Monad (e.toMonad m)

Equations

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

instance EffectKind.instLawfulMonadToMonad {e : EffectKind} {m : Type → Type} [Monad m] [LawfulMonad m] : LawfulMonad (e.toMonad m)

Equations

• ⋯ = ⋯

def EffectKind.return {m : Type → Type} {α : Type} [Monad m] (e : EffectKind) (a : α) : e.toMonad m α

Equations

• e.return a = pure a

@[simp]

def EffectKind.return_eq {m : Type → Type} {α : Type} [Monad m] (e : EffectKind) (a : α) : e.return a = pure a

Equations

• ⋯ = ⋯

@[simp]

def EffectKind.return_pure_toMonad_eq {α : Type} {m : Type → Type} (a : α) : pure a = a

Equations

• ⋯ = ⋯

@[simp]

def EffectKind.return_impure_toMonad_eq {m : Type → Type} {α : Type} [Monad m] (a : α) : pure a = pure a

Equations

• ⋯ = ⋯

PartialOrder

Establish a partial order on EffectKind

inductive EffectKind.le : EffectKind → EffectKind → Prop

• pure_le: ∀ (e : EffectKind), EffectKind.pure.le e
• le_impure: ∀ (e : EffectKind), e.le EffectKind.impure

def EffectKind.decLe (e : EffectKind) (e' : EffectKind) : Decidable (e.le e')

Equations

• EffectKind.pure.decLe EffectKind.pure = isTrue ⋯
• EffectKind.pure.decLe EffectKind.impure = isTrue ⋯
• EffectKind.impure.decLe EffectKind.pure = isFalse EffectKind.decLe.proof_1
• EffectKind.impure.decLe EffectKind.impure = isTrue ⋯

instance EffectKind.instLE : LE EffectKind

Equations

• EffectKind.instLE = { le := EffectKind.le }

instance EffectKind.instDecidableRelLe : DecidableRel LE.le

Equations

• EffectKind.instDecidableRelLe = EffectKind.decLe

@[simp]

theorem EffectKind.eq_of_le_pure {e : EffectKind} (he : e ≤ EffectKind.pure) : e = EffectKind.pure

@[simp]

theorem EffectKind.not_impure_le_pure : ¬EffectKind.impure ≤ EffectKind.pure

@[simp]

theorem EffectKind.pure_le (e : EffectKind) : EffectKind.pure ≤ e

@[simp]

theorem EffectKind.le_impure (e : EffectKind) : e ≤ EffectKind.impure

@[simp]

theorem EffectKind.le_refl (e : EffectKind) : e ≤ e

@[simp]

theorem EffectKind.le_trans {e1 : EffectKind} {e2 : EffectKind} {e3 : EffectKind} (h12 : e1 ≤ e2) (h23 : e2 ≤ e3) : e1 ≤ e3

@[simp]

theorem EffectKind.le_antisymm {e1 : EffectKind} {e2 : EffectKind} (h12 : e1 ≤ e2) (h21 : e2 ≤ e1) : e1 = e2

theorem EffectKind.le_of_eq {e1 : EffectKind} {e2 : EffectKind} (h : e1 = e2) : e1 ≤ e2

instance EffectKind.instPartialOrder : PartialOrder EffectKind

Equations

• EffectKind.instPartialOrder = PartialOrder.mk @EffectKind.le_antisymm

Lattice

EffectKind forms a lattice

def EffectKind.sup : EffectKind → EffectKind → EffectKind

Equations

• EffectKind.pure.sup EffectKind.pure = EffectKind.pure
• x✝.sup x = EffectKind.impure

instance EffectKind.instSup : Sup EffectKind

Equations

• EffectKind.instSup = { sup := EffectKind.sup }

def EffectKind.inf : EffectKind → EffectKind → EffectKind

Equations

• EffectKind.impure.inf EffectKind.impure = EffectKind.impure
• x✝.inf x = EffectKind.pure

instance EffectKind.instInf : Inf EffectKind

Equations

• EffectKind.instInf = { inf := EffectKind.inf }

@[simp]

theorem EffectKind.pure_sup_pure_eq : EffectKind.pure ⊔ EffectKind.pure = EffectKind.pure

@[simp]

theorem EffectKind.impure_sup_eq {e : EffectKind} : EffectKind.impure ⊔ e = EffectKind.impure

@[simp]

theorem EffectKind.sup_impure_eq {e : EffectKind} : e ⊔ EffectKind.impure = EffectKind.impure

@[simp]

theorem EffectKind.impure_inf_impure_eq : EffectKind.impure ⊓ EffectKind.impure = EffectKind.impure

@[simp]

theorem EffectKind.pure_inf_eq {e : EffectKind} : EffectKind.pure ⊓ e = EffectKind.pure

@[simp]

theorem EffectKind.inf_pure_eq {e : EffectKind} : e ⊓ EffectKind.pure = EffectKind.pure

instance EffectKind.instLattice : Lattice EffectKind

Equations

• EffectKind.instLattice = Lattice.mk EffectKind.instLattice.proof_4 EffectKind.instLattice.proof_5 EffectKind.instLattice.proof_6

liftEffect

def EffectKind.liftEffect {m : Type → Type} [Monad m] {e1 : EffectKind} {e2 : EffectKind} {α : Type} (hle : e1 ≤ e2) (v1 : e1.toMonad m α) : e2.toMonad m α

Lift a value wrapped in effect e1 into effect e2, given that e1 ≤ e2.

Said differently, this is a functor from the category of EffectKind (with e1 ≤ e2 as its arrows) to Lean (with e1.toMonad x → e2.toMonad x as its arrows).

Equations

• EffectKind.liftEffect x v1_2 = v1_2
• EffectKind.liftEffect x v1_2 = v1_2
• EffectKind.liftEffect x v1_2 = pure v1_2

instance EffectKind.instMonadLiftOfLe {m : Type → Type} {e1 : EffectKind} {e2 : EffectKind} (h : e1 ≤ e2) [Monad m] : MonadLiftT (e1.toMonad m) (e2.toMonad m)

Equations

• EffectKind.instMonadLiftOfLe h = { monadLift := fun {α : Type} => EffectKind.liftEffect h }

instance EffectKind.instMonadLiftTToMonadOfMonad (eff : EffectKind) {m : Type → Type} [Monad m] : MonadLiftT (eff.toMonad m) m

Equations

• eff.instMonadLiftTToMonadOfMonad = EffectKind.instMonadLiftOfLe ⋯

@[simp]

theorem EffectKind.liftEffect_rfl {m : Type → Type} {eff : EffectKind} {α : Type} [Monad m] (hle : eff ≤ eff) : EffectKind.liftEffect hle = id

@[simp]

theorem EffectKind.liftEffect_pure_impure {m : Type → Type} {α : Type} [Monad m] (hle : EffectKind.pure ≤ EffectKind.impure) : EffectKind.liftEffect hle = pure

theorem EffectKind.liftEffect_eq_pure_cast {α : Type} {m : Type → Type} [Monad m] {eff : EffectKind} (eff_eq : eff = EffectKind.pure) (eff_le : eff ≤ EffectKind.impure) : EffectKind.liftEffect eff_le = fun (x : eff.toMonad m α) => pure (cast ⋯ x)

Forded version of liftEffect_pure_impure

@[simp]

theorem EffectKind.liftEffect_pure {m : Type → Type} {α : Type} [Monad m] {e : EffectKind} (hle : e ≤ EffectKind.pure) : EffectKind.liftEffect hle = cast ⋯

@[simp]

theorem EffectKind.liftEffect_impure {m : Type → Type} {α : Type} [Monad m] {e : EffectKind} (hle : e ≤ EffectKind.impure) : EffectKind.liftEffect hle = match (motive := (e : EffectKind) → e ≤ EffectKind.impure → e.toMonad m α → EffectKind.impure.toMonad m α) e, hle with | EffectKind.pure, hle => fun (v : EffectKind.pure.toMonad m α) => pure v | EffectKind.impure, hle => id

@[simp]

theorem EffectKind.liftEffect_eq_id {eff : EffectKind} {m : Type → Type} {α : Type} (hle : eff ≤ eff) [Monad m] : EffectKind.liftEffect hle = id

toMonad is functorial: it preserves identity.

def EffectKind.liftEffect_compose {m : Type → Type} {e1 : EffectKind} {e2 : EffectKind} {e3 : EffectKind} {α : Type} [Monad m] (h12 : e1 ≤ e2) (h23 : e2 ≤ e3) (h13 : optParam (e1 ≤ e3) ⋯) : EffectKind.liftEffect h23 ∘ EffectKind.liftEffect h12 = EffectKind.liftEffect h13

toMonad is functorial: it preserves composition.

Equations

• ⋯ = ⋯