max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/init/meta/tactic): add applyc tactic

Browse source
This commit is contained in:
Leonardo de Moura 2017-02-25 12:55:28 -08:00
parent 7ec0505e94
commit 04e27eb96f
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/init/meta/tactic.lean
View file

@ -769,6 +769,10 @@ do env ← get_env,
ls ← mk_num_meta_univs num,
return (expr.const c ls)
/-- Apply the constant `c` -/
meta def applyc (c : name) : tactic unit :=
mk_const c >>= apply
meta def save_const_type_info (n : name) (ref : expr) : tactic unit :=
try (do c ← mk_const n, save_type_info c ref)