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

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

Browse source
This commit is contained in:
Johannes Hölzl 2017-02-20 11:14:51 -05:00 • committed by Leonardo de Moura
parent da4f552a7a
commit ca0fe37c41
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -804,6 +804,13 @@ return $ expr.local_const uniq_name pp_name bi type
meta def mk_local_def (pp_name : name) (type : expr) : tactic expr :=
mk_local' pp_name binder_info.default type
meta def mk_local_pis : expr → tactic (list expr × expr)
| (expr.pi n bi d b) := do
p ← mk_local' n bi d,
(ps, r) ← mk_local_pis (expr.instantiate_var b p),
return ((p :: ps), r)
| e := return ([], e)
private meta def get_pi_arity_aux : expr → tactic nat
| (expr.pi n bi d b) :=
do m ← mk_fresh_name,