-
Notifications
You must be signed in to change notification settings - Fork 251
/
SynthesizeUsing.lean
66 lines (53 loc) · 1.97 KB
/
SynthesizeUsing.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
/-
Copyright (c) 2022 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison
-/
import Lean
/-!
# `SynthesizeUsing`
This is a slight simplification of the `solve_aux` tactic in Lean3.
-/
open Lean Elab Tactic Meta
/--
`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.
-/
-- In Lean3 this was called `solve_aux`,
-- and took a `TacticM α` and captured the produced value in `α`.
-- As this was barely used, we've simplified here.
def synthesizeUsing (type : Expr) (tac : TacticM Unit) : MetaM (List MVarId × Expr) := do
let m ← mkFreshExprMVar type
let goals ← (run m.mvarId! tac).run'
return (goals, ← instantiateMVars m)
/--
`synthesizeUsing type tac` synthesizes an element of type `type` using tactic `tac`.
The tactic must solve for all goals, in contrast to `synthesizeUsing`.
-/
def synthesizeUsing' (type : Expr) (tac : TacticM Unit) : MetaM Expr := do
let (_, e) ← synthesizeUsing type (tac *> Tactic.done)
return e
/--
`synthesizeUsing type tacticSyntax` synthesizes an element of type `type` by evaluating the
given tactic syntax.
Example:
```lean
let (gs, e) ← synthesizeUsing ty (← `(tactic| congr!))
```
The tactic `tac` is allowed to leave goals open, and these remain as metavariables in the
returned expression.
-/
def synthesizeUsingTactic (type : Expr) (tac : Syntax) : MetaM (List MVarId × Expr) := do
synthesizeUsing type (do evalTactic tac)
/--
`synthesizeUsing' type tacticSyntax` synthesizes an element of type `type` by evaluating the
given tactic syntax.
Example:
```lean
let e ← synthesizeUsing ty (← `(tactic| norm_num))
```
The tactic must solve for all goals, in contrast to `synthesizeUsingTactic`.
-/
def synthesizeUsingTactic' (type : Expr) (tac : Syntax) : MetaM Expr := do
synthesizeUsing' type (do evalTactic tac)