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

- name : Name
- uniq : Name
- p : Expr

Instances For

source
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

Instances For

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

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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

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

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

Instances For

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

Instances For

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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

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

Instances For

source
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)

Instances For

source
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)

Instances For

source
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

Instances For

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

Instances For

source
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

Instances For

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

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

Instances For

source
def Lean.Elab.Tactic.Do.ProofMode.instInhabitedMGoal.default :
MGoal
Equations

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

Instances For

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

- Lean.Elab.Tactic.Do.ProofMode.instInhabitedMGoal = { default := Lean.Elab.Tactic.Do.ProofMode.instInhabitedMGoal.default }

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

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

Instances For

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

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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

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

Instances For

source
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

Instances For

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

Instances For

source
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

Instances For

source
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)

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For