Documentation

Lean.Elab.Tactic.LibrarySearch

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
    Instances For
      source
      def Lean.Elab.LibrarySearch.evalExact :
      Tactic.Tactic
      Equations
        Instances For
          source
          def Lean.Elab.LibrarySearch.evalApply :
          Tactic.Tactic
          Equations
            Instances For
              source
              def Lean.Elab.LibrarySearch.elabExact?Term :
              Term.TermElab
              Equations
                Instances For