# `SynthesizeUsing` #

This is a slight simplification of the `solve_aux` tactic in Lean3.

source
def synthesizeUsing {u : Lean.Level} (type : Q(Sort u)) (tac : Lean.Elab.Tactic.TacticM Unit) :
Lean.MetaM (List Lean.MVarId × Q(«$type»))

`synthesizeUsing type tac` synthesizes an element of type `type` using tactic `tac`.

The tactic `tac` is allowed to leave goals open, and these remain as metavariables in the returned expression.

Equations

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

Instances For

source
def synthesizeUsing' {u : Lean.Level} (type : Q(Sort u)) (tac : Lean.Elab.Tactic.TacticM Unit) :
Lean.MetaM Q(«$type»)

`synthesizeUsing type tac` synthesizes an element of type `type` using tactic `tac`.

The tactic must solve for all goals, in contrast to `synthesizeUsing`.

Equations

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

Instances For

source
def synthesizeUsingTactic {u : Lean.Level} (type : Q(Sort u)) (tac : Lean.Syntax) :
Lean.MetaM (List Lean.MVarId × Q(«$type»))

`synthesizeUsing type tacticSyntax` synthesizes an element of type `type` by evaluating the given tactic syntax.

Example:

    let (gs, e) ← synthesizeUsingTactic ty (← `(tactic| congr!))

The tactic `tac` is allowed to leave goals open, and these remain as metavariables in the returned expression.

Equations

- synthesizeUsingTactic type tac = synthesizeUsing type (Lean.Elab.Tactic.evalTactic tac)

Instances For

source
def synthesizeUsingTactic' {u : Lean.Level} (type : Q(Sort u)) (tac : Lean.Syntax) :
Lean.MetaM Q(«$type»)

`synthesizeUsing' type tacticSyntax` synthesizes an element of type `type` by evaluating the given tactic syntax.

Example:

    let e ← synthesizeUsingTactic' ty (← `(tactic| norm_num))

The tactic must solve for all goals, in contrast to `synthesizeUsingTactic`.

If you need to insert expressions into a tactic proof, then you might use `synthesizeUsing'` directly, since the `TacticM` monad has access to the `TermElabM` monad. For example, here is a term elaborator that wraps the `simp at ...` tactic:

    def simpTerm (e : Expr) : MetaM Expr := do
      let mvar ← Meta.mkFreshTypeMVar
      let e' ← synthesizeUsing' mvar
        (do evalTactic (← `(tactic| have h := $(← Term.exprToSyntax e); simp at h; exact h)))
      -- Note: `simp` does not always insert type hints, so to ensure that we get a term
      -- with the simplified type (as opposed to one that is merely defeq), we should add
      -- a type hint ourselves.
      Meta.mkExpectedTypeHint e' mvar

    elab "simpTerm% " t:term : term => do simpTerm (← Term.elabTerm t none)

Equations

- synthesizeUsingTactic' type tac = synthesizeUsing' type (Lean.Elab.Tactic.evalTactic tac)

Instances For