@[match_pattern]

def Iris.ProofMode.nameAnnotation : Lean.Name

Equations

• Iris.ProofMode.nameAnnotation = `name

@[match_pattern]

def Iris.ProofMode.uniqAnnotation : Lean.Name

Equations

• Iris.ProofMode.uniqAnnotation = `uniq

def Iris.ProofMode.parseName? : Lean.Expr → Option (Lean.Name × Lean.Name × Lean.Expr)

Equations

• Iris.ProofMode.parseName? (Lean.Expr.mdata { entries := [(`name, Lean.DataValue.ofName name), (`uniq, Lean.DataValue.ofName uniq)] } e) = some (name, uniq, e)
• Iris.ProofMode.parseName? x✝ = none

def Iris.ProofMode.mkNameAnnotation (name uniq : Lean.Name) (e : Lean.Expr) : Lean.Expr

Equations

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

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

• emp {u : Lean.Level} {prop : Q(Type u)} {bi : Q(BI «$prop»)} {e : Q(«$prop»)} : «$e» =Q iprop(emp) → Hyps bi e
• sep {u : Lean.Level} {prop : Q(Type u)} {bi : Q(BI «$prop»)} {e : Q(«$prop»)} (tm elhs erhs : Q(«$prop»)) : «$e» =Q iprop(«$elhs» ∗ «$erhs») → (lhs : Hyps bi elhs) → (rhs : Hyps bi erhs) → Hyps bi e
• hyp {u : Lean.Level} {prop : Q(Type u)} {bi : Q(BI «$prop»)} {e : Q(«$prop»)} (tm : Q(«$prop»)) (name uniq : Lean.Name) (p : Q(Bool)) (ty : Q(«$prop»)) : «$e» =Q iprop(□?«$p» «$ty») → Hyps bi e

instance Iris.ProofMode.instInhabitedHyps {a✝ : Lean.Level} {arg✝ : Q(Type a✝)} {bi : Q(BI $arg✝)} {s : Q($arg✝)} : Inhabited (Hyps bi s)

Equations

• Iris.ProofMode.instInhabitedHyps = { default := Iris.ProofMode.Hyps.emp ⋯ }

def Iris.ProofMode.Hyps.tm {a✝ : Lean.Level} {prop : Q(Type a✝)} {bi : Q(BI «$prop»)} {s : Q(«$prop»)} : Hyps bi s → Q(«$prop»)

Equations

• (Iris.ProofMode.Hyps.emp x_1).tm = s
• (Iris.ProofMode.Hyps.sep tm elhs erhs x_1 lhs rhs).tm = tm
• (Iris.ProofMode.Hyps.hyp tm name uniq p ty x_1).tm = tm

def Iris.ProofMode.Hyps.mkEmp {u : Lean.Level} {prop : Q(Type u)} (bi : Q(BI «$prop»)) (e : Q(«$prop») := q(iprop(emp))) : Hyps bi e

Equations

• Iris.ProofMode.Hyps.mkEmp bi e = Iris.ProofMode.Hyps.emp ⋯

def Iris.ProofMode.Hyps.mkSep {u : Lean.Level} {prop : Q(Type u)} {bi : Q(BI «$prop»)} {elhs erhs : Q(«$prop»)} (lhs : Hyps bi elhs) (rhs : Hyps bi erhs) (e : Q(«$prop») := q(iprop(«$elhs» ∗ «$erhs»))) : Hyps bi e

Equations

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

def Iris.ProofMode.isTrue (p : Q(Bool)) : Bool

Equations

• Iris.ProofMode.isTrue p = (Lean.Expr.constName! p == `Bool.true)

def Iris.ProofMode.matchBool (p : Q(Bool)) : «$p» =Q true ⊕' «$p» =Q false

Equations

• Iris.ProofMode.matchBool p = if Iris.ProofMode.isTrue p = true then PSum.inl ⋯ else PSum.inr ⋯

def Iris.ProofMode.mkIntuitionisticIf {u : Lean.Level} {prop : Q(Type u)} (_bi : Q(BI «$prop»)) (p : Q(Bool)) (e : Q(«$prop»)) : { A : Q(«$prop») // «$A» =Q iprop(□?«$p» «$e») }

Equations

• Iris.ProofMode.mkIntuitionisticIf _bi p e = match Iris.ProofMode.matchBool p with | PSum.inl val => ⟨q(iprop(□ «$e»)), ⋯⟩ | PSum.inr val => ⟨e, ⋯⟩

def Iris.ProofMode.Hyps.mkHyp {u : Lean.Level} {prop : Q(Type u)} (bi : Q(BI «$prop»)) (name uniq : Lean.Name) (p : Q(Bool)) (ty : Q(«$prop»)) (e : Q(«$prop») := q(iprop(□?«$p» «$ty»))) : Hyps bi e

Equations

• Iris.ProofMode.Hyps.mkHyp bi name uniq p ty e = Iris.ProofMode.Hyps.hyp (Iris.ProofMode.mkIntuitionisticIf bi p (Iris.ProofMode.mkNameAnnotation name uniq ty)).val name uniq p ty ⋯

partial def Iris.ProofMode.parseHyps? {u : Lean.Level} {prop : Q(Type u)} (bi : Q(BI «$prop»)) (expr : Lean.Expr) : Option ((s : Q(«$prop»)) × Hyps bi s)

partial def Iris.ProofMode.Hyps.find? {u : Lean.Level} {prop : Q(Type u)} {bi : Q(BI «$prop»)} (name : Lean.Name) {s : Q(«$prop»)} : Hyps bi s → Option (Lean.Name × Q(Bool) × Q(«$prop»))

@[reducible, inline]

abbrev Iris.ProofMode.Entails' {PROP : Type u_1} [BI PROP] : PROP → PROP → Prop

This is the same as Entails, but it takes a BI instead. This constant is used to detect iris proof goals.

Equations

• Iris.ProofMode.Entails' = Iris.BI.Entails

structure Iris.ProofMode.IrisGoal : Type

• u : Lean.Level
• prop : Q(Type udummy._uniq.21)
• bi : Q(BI unknown_1)
• e : Q(unknown_1)
• hyps : Hyps self.bi self.e
• goal : Q(unknown_1)

def Iris.ProofMode.isIrisGoal (expr : Lean.Expr) : Bool

Equations

• Iris.ProofMode.isIrisGoal expr = expr.isAppOfArity `Iris.ProofMode.Entails' 4

def Iris.ProofMode.parseIrisGoal? (expr : Lean.Expr) : Option IrisGoal

def Iris.ProofMode.IrisGoal.toExpr : IrisGoal → Lean.Expr

Equations

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

def Iris.ProofMode.IrisGoal.strip : IrisGoal → Lean.Expr

Equations

• { u := u, prop := prop, bi := bi, e := e, hyps := hyps, goal := goal }.strip = q(«$e» ⊢ «$goal»)

def Iris.ProofMode.HypMarker {PROP : Type u_1} (_A : PROP) : Prop

This is only used for display purposes, so that we can render context variables that appear to have type A : PROP even though PROP is not a type.

Equations

• Iris.ProofMode.HypMarker _A = True

def Iris.ProofMode.addLocalVarInfo (stx : Lean.Syntax) (lctx : Lean.LocalContext) (expr : Lean.Expr) (expectedType? : Option Lean.Expr) (isBinder : Bool := false) : Lean.MetaM Unit

Equations

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

def Iris.ProofMode.addHypInfo {u : Lean.Level} (stx : Lean.Syntax) (name uniq : Lean.Name) (prop : Q(Type u)) (ty : Q(«$prop»)) (isBinder : Bool := false) : Lean.MetaM Unit

Equations

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

def Iris.ProofMode.Hyps.findWithInfo {s : Lean.Expr} {u : Lean.Level} {prop : Q(Type u)} {bi : Q(BI «$prop»)} (hyps : Hyps bi s) (name : Lean.Ident) : Lean.MetaM Lean.Name

Equations

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