Documentation

Iris.ProofMode.Display

source
def Iris.ProofMode.irisHyp :
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Iris.ProofMode.irisGoalStx :
    Lean.ParserDescr
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Iris.ProofMode.delabIrisGoal :
      Lean.PrettyPrinter.Delaborator.Delab
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Iris.ProofMode.delabIrisGoal.delabHypotheses {u : Lean.Level} {prop : Q(Type u)} {bi : Q(BI «$prop»)} {s : Q(«$prop»)} (hyps : Hyps bi s) (acc : Lean.NameMap Nat × Array (Lean.TSyntax `Iris.ProofMode.irisHyp)) :
        Lean.PrettyPrinter.Delaborator.DelabM (Lean.NameMap Nat × Array (Lean.TSyntax `Iris.ProofMode.irisHyp))
        Equations
        Instances For
          source
          def Iris.ProofMode.delabHypMarker :
          Lean.PrettyPrinter.Delaborator.Delab
          Equations
          Instances For