theorem Iris.ProofMode.pure_assumption {PROP : Type u_1} [BI PROP] {P A Q : PROP} (h_P : ⊢ A) [inst : FromAssumption true A Q] [Std.TCOr (BI.Affine P) (BI.Absorbing Q)] : P ⊢ Q

def Iris.ProofMode.assumptionLean {u : Lean.Level} {prop : Q(Type u)} (_bi : Q(BI «$prop»)) (ehyps goal : Q(«$prop»)) (mvar : Lean.MVarId) : Lean.MetaM Unit

Equations

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

def Iris.ProofMode.tacticIassumption_lean : Lean.ParserDescr

Equations

• Iris.ProofMode.tacticIassumption_lean = Lean.ParserDescr.node `Iris.ProofMode.tacticIassumption_lean 1024 (Lean.ParserDescr.nonReservedSymbol "iassumption_lean" false)

inductive Iris.ProofMode.AssumptionFastPath {u : Lean.Level} (prop : Q(Type u)) (bi : Q(BI «$prop»)) (Q : Q(«$prop»)) : Type

• absorbing {u : Lean.Level} {prop : Q(Type u)} {bi : Q(BI «$prop»)} {Q : Q(«$prop»)} : Q(BI.Absorbing «$Q») → AssumptionFastPath prop bi Q
• biAffine {u : Lean.Level} {prop : Q(Type u)} {bi : Q(BI «$prop»)} {Q : Q(«$prop»)} : Q(BI.BIAffine «$prop») → AssumptionFastPath prop bi Q

def Iris.ProofMode.assumptionFast {u : Lean.Level} {prop : Q(Type u)} (bi : Q(BI «$prop»)) (Q : Q(«$prop»)) (fastPath : AssumptionFastPath prop bi Q) {e : Q(«$prop»)} (hyps : Hyps bi e) : Lean.MetaM Q(«$e» ⊢ «$Q»)

Equations

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

inductive Iris.ProofMode.AssumptionSlow {u : Lean.Level} {prop : Q(Type u)} (bi : Q(BI «$prop»)) (Q e : Q(«$prop»)) : Type

• none {u : Lean.Level} {prop : Q(Type u)} {bi : Q(BI «$prop»)} {Q e : Q(«$prop»)} : AssumptionSlow bi Q e
• affine {u : Lean.Level} {prop : Q(Type u)} {bi : Q(BI «$prop»)} {Q e : Q(«$prop»)} (pf : Q(BI.Affine «$e»)) : AssumptionSlow bi Q e
• main {u : Lean.Level} {prop : Q(Type u)} {bi : Q(BI «$prop»)} {Q e : Q(«$prop»)} (pf : Q(«$e» ⊢ «$Q»)) : Option Q(BI.Affine «$e») → AssumptionSlow bi Q e

theorem Iris.ProofMode.assumption_l {PROP : Type u_1} [BI PROP] {P Q R : PROP} [BI.Affine Q] (h : P ⊢ R) : P ∗ Q ⊢ R

theorem Iris.ProofMode.assumption_r {PROP : Type u_1} [BI PROP] {P Q R : PROP} [BI.Affine P] (h : Q ⊢ R) : P ∗ Q ⊢ R

def Iris.ProofMode.assumptionSlow {u : Lean.Level} {prop : Q(Type u)} (bi : Q(BI «$prop»)) (Q : Q(«$prop»)) (assume : Bool) {e : Q(«$prop»)} : Hyps bi e → Lean.MetaM (AssumptionSlow bi Q e)

Equations

• One or more equations did not get rendered due to their size.
• Iris.ProofMode.assumptionSlow bi Q assume (Iris.ProofMode.Hyps.emp x_3) = pure (Iris.ProofMode.AssumptionSlow.affine q(⋯))

def Iris.ProofMode.tacticIassumption : Lean.ParserDescr

Equations

• Iris.ProofMode.tacticIassumption = Lean.ParserDescr.node `Iris.ProofMode.tacticIassumption 1024 (Lean.ParserDescr.nonReservedSymbol "iassumption" false)