SynthesizeUsing

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

ink

def synthesizeUsing (type : Lean.Expr) (tac : Lean.Elab.Tactic.TacticM Unit) : Lean.MetaM Lean.Expr

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

The tactic tac may leave goals open, these remain as metavariables in the returned expression.

Equations

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