def Lean.Elab.LibrarySearch.exact? (ref : Lean.Syntax) (required : Option (Array (Lean.TSyntax `term))) (requireClose : Bool) : Lean.Elab.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.evalExact : Lean.Elab.Tactic.Tactic

Equations

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

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

Equations

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

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