Documentation

Iris.ProofMode.Tactics.Basic

source
def Iris.ProofMode.istart (mvar : Lean.MVarId) :
Lean.MetaM (Lean.MVarId × IrisGoal)
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Iris.ProofMode.tacticIstart :
    Lean.ParserDescr
    Equations
    Instances For
      source
      def Iris.ProofMode.tacticIstop :
      Lean.ParserDescr
      Equations
      Instances For
        source
        theorem Iris.ProofMode.assumption {PROP : Type u_1} [BI PROP] {p : Bool} {P P' A Q : PROP} [inst : FromAssumption p A Q] [Std.TCOr (BI.Affine P') (BI.Absorbing Q)] (h : P ⊣⊢ P' ∗ □?p A) :
        P ⊢ Q
        source
        def Iris.ProofMode.getFreshName :
        Lean.TSyntax `Lean.binderIdent → Lean.CoreM (Lean.Name × Lean.Syntax)
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Iris.ProofMode.selectHyp {u : Lean.Level} {prop : Q(Type u)} {bi : Q(BI «$prop»)} (ty : Lean.Expr) {s : Q(«$prop»)} :
          Hyps bi s → Lean.MetaM (Lean.Name × Q(Bool) × Q(«$prop»))
          Equations
          Instances For