-
Notifications
You must be signed in to change notification settings - Fork 0
/
tactics.lean
27 lines (22 loc) · 1.01 KB
/
tactics.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
import meta.expr
import tactic.basic
meta def name.update_suffix : name → (string → string) → name
| name.anonymous _ := name.anonymous
| (name.mk_string s p) f := name.mk_string (f s) p
| (name.mk_numeral n p) _ := name.mk_numeral n p
namespace tactic ---------------------------------------------------------------
namespace interactive ----------------------------------------------------------
open interactive
open interactive.types
meta def note_all_applied (p : parse texpr) : tactic unit :=
do e ← to_expr p,
et ← infer_type e,
guard et.is_pi <|> fail format!"'note_all_applied' expects a function, got '{et}'",
ctx ← local_context,
ctx.for_each $ λ h, do
ht ← infer_type h,
tactic.try $ do
unify ht et.binding_domain,
note (h.local_pp_name.update_suffix (++ "'")) none (e.mk_app [h])
end /- namespace -/ interactive ------------------------------------------------
end /- namespace -/ tactic -----------------------------------------------------