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

fix(init/meta/constructor_tactic): constructor tac uses whnf

Browse source
This commit is contained in:
Mario Carneiro 2017-06-19 03:56:14 -04:00 • committed by Leonardo de Moura
parent d0242a3631
commit 1e2157e210
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/meta/constructor_tactic.lean
View file

@ -19,7 +19,7 @@ private meta def try_constructors (cfg : apply_cfg): list name → tactic unit
| (c::cs) := (mk_const c >>= λ e, apply_core e cfg >> return ()) <|> try_constructors cs
meta def constructor (cfg : apply_cfg := {}): tactic unit :=
target >>= instantiate_mvars >>= get_constructors_for >>= try_constructors cfg
target >>= instantiate_mvars >>= whnf >>= get_constructors_for >>= try_constructors cfg
meta def econstructor : tactic unit :=
constructor {new_goals := new_goals.non_dep_only}