Documentation

Iris.ProofMode.Tactics.Pure

source
theorem Iris.ProofMode.pure_elim_spatial {PROP : Type u_1} [BI PROP] {P P' A Q : PROP} {φ : Prop} [hA : IntoPure A φ] [or : Std.TCOr (BI.Affine A) (BI.Absorbing Q)] (h : P ⊣⊢ P' ∗ A) (h_entails : φ → P' ⊢ Q) :
P ⊢ Q
source
theorem Iris.ProofMode.pure_elim_intuitionistic {PROP : Type u_1} [BI PROP] {P P' A Q : PROP} {φ : Prop} [IntoPure A φ] (h : P ⊣⊢ P' ∗ □ A) (h' : φ → P' ⊢ Q) :
P ⊢ Q
source
def Iris.ProofMode.ipureCore {u : Lean.Level} {α : Type} {prop : Q(Type u)} (_bi : Q(BI «$prop»)) (P P' A Q : Q(«$prop»)) (name : Lean.TSyntax `Lean.binderIdent) (pf : Q(«$P» ⊣⊢ «$P'» ∗ «$A»)) (k : (φ : Q(Prop)) → Q(«$φ») → Lean.MetaM (α × Q(«$P'» ⊢ «$Q»))) :
Lean.MetaM (α × Q(«$P» ⊢ «$Q»))
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Iris.ProofMode.tacticIpure__ :
    Lean.ParserDescr
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Iris.ProofMode.tacticIemp_intro :
      Lean.ParserDescr
      Equations
      Instances For
        source
        theorem Iris.ProofMode.pure_intro_affine {PROP : Type u_1} {P : PROP} [BI PROP] {Q : PROP} {φ : Prop} [h : FromPure true Q φ] [BI.Affine P] (hφ : φ) :
        P ⊢ Q
        source
        theorem Iris.ProofMode.pure_intro_spatial {PROP : Type u_1} {P : PROP} [BI PROP] {Q : PROP} {φ : Prop} [h : FromPure false Q φ] (hφ : φ) :
        P ⊢ Q
        source
        def Iris.ProofMode.tacticIpure_intro :
        Lean.ParserDescr
        Equations
        Instances For