structure Lean.Elab.Tactic.Do.ProofMode.Hyp : Type

• name : Name
• uniq : Name
• p : Expr

def Lean.Elab.Tactic.Do.ProofMode.parseHyp? : Expr → Option Hyp

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Tactic.Do.ProofMode.parseHyp? x✝ = none

def Lean.Elab.Tactic.Do.ProofMode.Hyp.toExpr (hyp : Hyp) : Expr

Equations

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

def Lean.Elab.Tactic.Do.ProofMode.SPred.mkType (u : Level) (σs : Expr) : Expr

Equations

• Lean.Elab.Tactic.Do.ProofMode.SPred.mkType u σs = Lean.mkApp (Lean.mkConst `Std.Do.SPred [u]) σs

def Lean.Elab.Tactic.Do.ProofMode.SPred.mkPure (u : Level) (σs p : Expr) : Expr

Equations

• Lean.Elab.Tactic.Do.ProofMode.SPred.mkPure u σs p = Lean.mkApp2 (Lean.mkConst `Std.Do.SPred.pure [u]) σs p

def Lean.Elab.Tactic.Do.ProofMode.SPred.isPure? : Expr → Option (Level × Expr × Expr)

Equations

• Lean.Elab.Tactic.Do.ProofMode.SPred.isPure? (((Lean.Expr.const `Std.Do.SPred.pure [u]).app σs).app p) = some (u, σs, p)
• Lean.Elab.Tactic.Do.ProofMode.SPred.isPure? x✝ = none

def Lean.Elab.Tactic.Do.ProofMode.emptyHypName : Name

Equations

• Lean.Elab.Tactic.Do.ProofMode.emptyHypName = `emptyHyp

def Lean.Elab.Tactic.Do.ProofMode.emptyHyp (u : Level) (σs : Expr) : Expr

Equations

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

def Lean.Elab.Tactic.Do.ProofMode.parseEmptyHyp? (e : Expr) : Option (Level × Expr)

Equations

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

def Lean.Elab.Tactic.Do.ProofMode.pushLeftConjunct (pos : SubExpr.Pos) : SubExpr.Pos

Equations

• Lean.Elab.Tactic.Do.ProofMode.pushLeftConjunct pos = Lean.SubExpr.Pos.pushNaryArg 3 1 pos

def Lean.Elab.Tactic.Do.ProofMode.pushRightConjunct (pos : SubExpr.Pos) : SubExpr.Pos

Equations

• Lean.Elab.Tactic.Do.ProofMode.pushRightConjunct pos = Lean.SubExpr.Pos.pushNaryArg 3 2 pos

def Lean.Elab.Tactic.Do.ProofMode.SPred.mkAnd! (u : Level) (σs lhs rhs : Expr) : Expr

Combine two hypotheses into a conjunction. Precondition: Neither lhs nor rhs is empty (parseEmptyHyp?).

Equations

• Lean.Elab.Tactic.Do.ProofMode.SPred.mkAnd! u σs lhs rhs = Lean.mkApp3 (Lean.mkConst `Std.Do.SPred.and [u]) σs lhs rhs

def Lean.Elab.Tactic.Do.ProofMode.SPred.mkAnd (u : Level) (σs lhs rhs : Expr) : Expr × Expr

Smart constructor that cancels away empty hypotheses, along with a proof that lhs ∧ rhs ⊣⊢ₛ result.

Equations

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

def Lean.Elab.Tactic.Do.ProofMode.TypeList.mkType (u : Level) : Expr

Equations

• Lean.Elab.Tactic.Do.ProofMode.TypeList.mkType u = Lean.mkApp (Lean.mkConst `List [u.succ]) (Lean.mkSort u.succ)

def Lean.Elab.Tactic.Do.ProofMode.TypeList.mkNil (u : Level) : Expr

Equations

• Lean.Elab.Tactic.Do.ProofMode.TypeList.mkNil u = Lean.mkApp (Lean.mkConst `List.nil [u.succ]) (Lean.mkSort u.succ)

def Lean.Elab.Tactic.Do.ProofMode.TypeList.mkCons (u : Level) (hd tl : Expr) : Expr

Equations

• Lean.Elab.Tactic.Do.ProofMode.TypeList.mkCons u hd tl = Lean.mkApp3 (Lean.mkConst `List.cons [u.succ]) (Lean.mkSort u.succ) hd tl

def Lean.Elab.Tactic.Do.ProofMode.TypeList.length (σs : Expr) : MetaM Nat

Equations

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

def Lean.Elab.Tactic.Do.ProofMode.parseAnd? (e : Expr) : Option (Level × Expr × Expr × Expr)

Equations

• Lean.Elab.Tactic.Do.ProofMode.parseAnd? e = (fun (x : Lean.Expr × Lean.Expr × Lean.Expr) => (e.getAppFn.constLevels![0]!, x)) <$> e.app3? `Std.Do.SPred.and

structure Lean.Elab.Tactic.Do.ProofMode.MGoal : Type

• u : Level
• σs : Expr
• hyps : Expr
• target : Expr

instance Lean.Elab.Tactic.Do.ProofMode.instInhabitedMGoal : Inhabited MGoal

Equations

• Lean.Elab.Tactic.Do.ProofMode.instInhabitedMGoal = { default := { u := default, σs := default, hyps := default, target := default } }

def Lean.Elab.Tactic.Do.ProofMode.parseMGoal? (expr : Expr) : Option MGoal

Equations

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

def Lean.Elab.Tactic.Do.ProofMode.ensureMGoal : TacticM (MVarId × MGoal)

Equations

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

def Lean.Elab.Tactic.Do.ProofMode.MGoal.strip (goal : MGoal) : Expr

Equations

• goal.strip = Lean.mkApp3 (Lean.mkConst `Std.Do.SPred.entails [goal.u]) goal.σs goal.hyps goal.target

def Lean.Elab.Tactic.Do.ProofMode.MGoal.toExpr (goal : MGoal) : Expr

Roundtrips with parseMGoal?.

Equations

• goal.toExpr = Lean.mkApp3 (Lean.mkConst `Std.Tactic.Do.MGoalEntails [goal.u]) goal.σs goal.hyps goal.target

def Lean.Elab.Tactic.Do.ProofMode.MGoal.findHyp? (goal : MGoal) (name : Name) : Option (SubExpr.Pos × Hyp)

Equations

• goal.findHyp? name = Lean.Elab.Tactic.Do.ProofMode.MGoal.findHyp?.go✝ name goal.hyps Lean.SubExpr.Pos.root

def Lean.Elab.Tactic.Do.ProofMode.checkHasType (expr expectedType : Expr) (suppressWarning : Bool := false) : MetaM Unit

Equations

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

def Lean.Elab.Tactic.Do.ProofMode.MGoal.checkProof (goal : MGoal) (prf : Expr) (suppressWarning : Bool := false) : MetaM Unit

Equations

• goal.checkProof prf suppressWarning = Lean.Elab.Tactic.Do.ProofMode.checkHasType prf goal.toExpr suppressWarning

def Lean.Elab.Tactic.Do.ProofMode.getFreshHypName : TSyntax `Lean.binderIdent → CoreM (Name × Syntax)

Equations

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

def Lean.Elab.Tactic.Do.ProofMode.pushForallContextIntoHyps (σs hyps : Expr) : Expr

Equations

• Lean.Elab.Tactic.Do.ProofMode.pushForallContextIntoHyps σs hyps = Lean.Elab.Tactic.Do.ProofMode.pushForallContextIntoHyps.go✝ σs #[] #[] hyps

def Lean.Elab.Tactic.Do.ProofMode.betaPreservingHypNames (σs' e : Expr) (args : Array Expr) : Expr

Equations

• Lean.Elab.Tactic.Do.ProofMode.betaPreservingHypNames σs' e args = Lean.Elab.Tactic.Do.ProofMode.pushForallContextIntoHyps σs' (Lean.mkAppN e args)

def Lean.Elab.Tactic.Do.ProofMode.dropStateList (σs : Expr) (n : Nat) : MetaM Expr

Equations

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

def Lean.Elab.Tactic.Do.ProofMode.MGoal.renameInaccessibleHyps (goal : MGoal) (idents : Array (TSyntax `Lean.binderIdent)) : MetaM MGoal

Equations

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

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

Equations

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

def Lean.Elab.Tactic.Do.ProofMode.addHypInfo (stx : Syntax) (σs : Expr) (hyp : Hyp) (isBinder : Bool := false) : MetaM Unit

Equations

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