Documentation

Lean.Elab.Tactic.ElabTerm

source
def Lean.Elab.Tactic.elabTerm (stx : Lean.Syntax) (expectedType? : Option Lean.Expr) (mayPostpone : optParam Bool false) :
Lean.Elab.Tactic.TacticM Lean.Expr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.elabTerm.go (stx : Lean.Syntax) (expectedType? : Option Lean.Expr) (mayPostpone : optParam Bool false) :
Lean.Elab.TermElabM Lean.Expr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.elabTermEnsuringType (stx : Lean.Syntax) (expectedType? : Option Lean.Expr) (mayPostpone : optParam Bool false) :
Lean.Elab.Tactic.TacticM Lean.Expr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.closeMainGoalUsing (x : Lean.Expr → Lean.Elab.Tactic.TacticM Lean.Expr) (checkUnassigned : optParam Bool true) :
Lean.Elab.Tactic.TacticM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.logUnassignedAndAbort (mvarIds : Array Lean.MVarId) :
Lean.Elab.Tactic.TacticM Unit
Equations
source
def Lean.Elab.Tactic.filterOldMVars (mvarIds : Array Lean.MVarId) (mvarCounterSaved : Nat) :
Lean.MetaM (Array Lean.MVarId)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.evalExact:
Lean.Elab.Tactic.Tactic
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.elabTermWithHoles (stx : Lean.Syntax) (expectedType? : Option Lean.Expr) (tagSuffix : Lean.Name) (allowNaturalHoles : optParam Bool false) :
Lean.Elab.Tactic.TacticM (Lean.Expr × List Lean.MVarId)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.refineCore (stx : Lean.Syntax) (tagSuffix : Lean.Name) (allowNaturalHoles : Bool) :
Lean.Elab.Tactic.TacticM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.evalRefine:
Lean.Elab.Tactic.Tactic
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.evalRefine':
Lean.Elab.Tactic.Tactic
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.evalSpecialize:
Lean.Elab.Tactic.Tactic
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.elabTermForApply (stx : Lean.Syntax) (mayPostpone : optParam Bool true) :
Lean.Elab.Tactic.TacticM Lean.Expr

Given a tactic

apply f

we want the apply tactic to create all metavariables. The following definition will return @f for f. That is, it will not create metavariables for implicit arguments. A similar method is also used in Lean 3. This method is useful when applying lemmas such as:

theorem infLeRight {s t : Set α} : s ⊓ t ≤ t

where s ≤ t here is defined as

∀ {x : α}, x ∈ s → x ∈ t
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.evalApplyLikeTactic (tac : Lean.MVarId → Lean.Expr → Lean.MetaM (List Lean.MVarId)) (e : Lean.Syntax) :
Lean.Elab.Tactic.TacticM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.getFVarId (id : Lean.Syntax) :
Lean.Elab.Tactic.TacticM Lean.FVarId
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.getFVarIds (ids : Array Lean.Syntax) :
Lean.Elab.Tactic.TacticM (Array Lean.FVarId)
Equations
source
def Lean.Elab.Tactic.evalApply:
Lean.Elab.Tactic.Tactic
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.evalConstructor:
Lean.Elab.Tactic.Tactic
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.evalWithReducible:
Lean.Elab.Tactic.Tactic
Equations
source
def Lean.Elab.Tactic.evalWithReducibleAndInstances:
Lean.Elab.Tactic.Tactic
Equations
source
def Lean.Elab.Tactic.evalWithUnfoldingAll:
Lean.Elab.Tactic.Tactic
Equations
source
def Lean.Elab.Tactic.elabAsFVar (stx : Lean.Syntax) (userName? : optParam (Option Lean.Name) none) :
Lean.Elab.Tactic.TacticM Lean.FVarId

Elaborate stx. If it a free variable, return it. Otherwise, assert it, and return the free variable. Note that, the main goal is updated when Meta.assert is used in the second case.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.evalRename:
Lean.Elab.Tactic.Tactic
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.evalDecide:
Lean.Elab.Tactic.Tactic
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.evalNativeDecide:
Lean.Elab.Tactic.Tactic
Equations
  • One or more equations did not get rendered due to their size.