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

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

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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