-
Notifications
You must be signed in to change notification settings - Fork 251
/
Recall.lean
78 lines (71 loc) · 3.13 KB
/
Recall.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
67
68
69
70
71
72
73
74
75
76
77
78
/-
Copyright (c) 2023 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone, Kyle Miller
-/
import Lean.Elab.Command
import Lean.Elab.DeclUtil
/-!
# `recall` command
-/
namespace Mathlib.Tactic.Recall
/--
The `recall` command redeclares a previous definition for illustrative purposes.
This can be useful for files that give an expository account of some theory in Lean.
The syntax of the command mirrors `def`, so all the usual bells and whistles work.
```
recall List.cons_append (a : α) (as bs : List α) : (a :: as) ++ bs = a :: (as ++ bs) := rfl
```
Also, one can leave out the body.
```
recall Nat.add_comm (n m : Nat) : n + m = m + n
```
The command verifies that the new definition type-checks and that the type and value
provided are definitionally equal to the original declaration. However, this does not
capture some details (like binders), so the following works without error.
```
recall Nat.add_comm {n m : Nat} : n + m = m + n
```
-/
syntax (name := recall) "recall " ident ppIndent(optDeclSig) (declVal)? : command
open Lean Meta Elab Command Term
elab_rules : command
| `(recall $id $sig:optDeclSig $[$val?]?) => withoutModifyingEnv do
let declName := id.getId
let some info := (← getEnv).find? declName
| throwError "unknown constant '{declName}'"
let declConst : Expr := mkConst declName <| info.levelParams.map Level.param
discard <| liftTermElabM <| addTermInfo id declConst
let newId := mkIdentFrom id (← mkAuxName declName 1)
if let some val := val? then
let some infoVal := info.value?
| throwErrorAt val "constant '{declName}' has no defined value"
elabCommand <| ← `(noncomputable def $newId $sig:optDeclSig $val)
let some newInfo := (← getEnv).find? newId.getId | return -- def already threw
liftTermElabM do
let mvs ← newInfo.levelParams.mapM fun _ => mkFreshLevelMVar
let newType := newInfo.type.instantiateLevelParams newInfo.levelParams mvs
unless (← isDefEq info.type newType) do
throwTypeMismatchError none info.type newInfo.type declConst
let newVal := newInfo.value?.get!.instantiateLevelParams newInfo.levelParams mvs
unless (← isDefEq infoVal newVal) do
let err := m!"\
value mismatch{indentExpr declConst}\nhas value{indentExpr newVal}\n\
but is expected to have value{indentExpr infoVal}"
throwErrorAt val err
else
let (binders, type?) := expandOptDeclSig sig
if let some type := type? then
runTermElabM fun vars => do
withAutoBoundImplicit do
elabBinders binders.getArgs fun xs => do
let xs ← addAutoBoundImplicits xs
let type ← elabType type
Term.synthesizeSyntheticMVarsNoPostponing
let type ← mkForallFVars xs type
let type ← mkForallFVars vars type (usedOnly := true)
unless (← isDefEq info.type type) do
throwTypeMismatchError none info.type type declConst
else
unless binders.getNumArgs == 0 do
throwError "expected type after ':'"