@[match_pattern]

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

Equations

• Lean.Elab.Tactic.Do.ProofMode.nameAnnotation = `name

@[match_pattern]

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

Equations

• Lean.Elab.Tactic.Do.ProofMode.uniqAnnotation = `uniq

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.emptyHyp (σs : Expr) : Expr

Equations

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

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

Equations

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

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.mkAnd! (σ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.mkAnd! σs lhs rhs = Lean.mkApp3 (Lean.mkConst `Std.Do.SPred.and) σs lhs rhs

def Lean.Elab.Tactic.Do.ProofMode.mkAnd (σ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.σs.mkType : Expr

Equations

• Lean.Elab.Tactic.Do.ProofMode.σs.mkType = Lean.mkApp (Lean.mkConst `List [Lean.Level.zero.succ]) (Lean.mkSort Lean.Level.zero.succ)

def Lean.Elab.Tactic.Do.ProofMode.σs.mkNil : Expr

Equations

• Lean.Elab.Tactic.Do.ProofMode.σs.mkNil = Lean.mkApp (Lean.mkConst `List.nil [Lean.Level.zero.succ]) (Lean.mkSort Lean.Level.zero.succ)

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

Equations

• Lean.Elab.Tactic.Do.ProofMode.parseAnd? e = (e.app3? `Std.Do.SPred.and <|> (fun (x : Lean.Expr × Lean.Expr) => (Lean.Elab.Tactic.Do.ProofMode.σs.mkNil, x)) <$> e.app2? `And)

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

• σs : Expr
• hyps : Expr
• target : Expr

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

Equations

• Lean.Elab.Tactic.Do.ProofMode.instInhabitedMGoal = { 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.σ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.σ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

partial def Lean.Elab.Tactic.Do.ProofMode.MGoal.findHyp?.go (name : Name) (e : Expr) (p : SubExpr.Pos) : Option (SubExpr.Pos × Hyp)

def Lean.Elab.Tactic.Do.ProofMode.MGoal.checkProof (goal : MGoal) (prf : 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.getFreshHypName : TSyntax `Lean.binderIdent → CoreM (Name × Syntax)

Equations

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

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

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.betaRevPreservingHypNames σs' e args.reverse

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.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.