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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For