def Lean.Elab.LibrarySearch.exact? (ref : Syntax) (required : Option (Array (TSyntax `term))) (requireClose : Bool) : Tactic.TacticM Unit

Implementation of the exact? tactic.

• ref contains the input syntax and is used for locations in error reporting.
• required contains an optional list of terms that should be used in closing the goal.
• requireClose indicates if the goal must be closed. It is true for exact? and false for apply?.

Equations

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

def Lean.Elab.LibrarySearch.exact?.evalTacticWithState (savedState : Tactic.SavedState) (tac : TSyntax `tactic) : Tactic.TacticM Unit

Executes tac in savedState (then restores the current state). Used to ensure that a suggested tactic is valid.

Remark: we don't merely elaborate the proof term's syntax because it may successfully round-trip (d)elaboration but still produce an invalid tactic (see the example in #5407).

Equations

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

def Lean.Elab.LibrarySearch.exact?.addSuggestionIfValid (ref : Syntax) (goal : MVarId) (initialState : Tactic.SavedState) (addSubgoalsMsg : Bool := false) (errorOnInvalid : Bool := true) : Tactic.TacticM Unit

Suggests using the value of goal as a proof term if the corresponding tactic is valid at origGoal, or else informs the user that a proof exists but is not syntactically valid.

Equations

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

def Lean.Elab.LibrarySearch.evalExact : Tactic.Tactic

Equations

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

def Lean.Elab.LibrarySearch.evalApply : Tactic.Tactic

Equations

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

def Lean.Elab.LibrarySearch.elabExact?Term : Term.TermElab

Equations

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