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

fix(library/init/meta/smt/interactive): adapt to wildcards in locations

Browse source
This commit is contained in:
Jeremy Avigad 2017-05-29 15:22:35 -04:00 • committed by Leonardo de Moura
parent 649118c99a
commit 1fa7c2285e
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/init/meta/smt/interactive.lean
View file

@ -229,7 +229,7 @@ open tactic
/-- Simplify the target type of the main goal. -/
meta def simp (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (cfg : simp_config := {}) : smt_tactic unit :=
tactic.interactive.simp hs attr_names ids [] cfg
tactic.interactive.simp hs attr_names ids (loc.ns []) cfg
/-- Simplify the target type of the main goal using simplification lemmas and the current set of hypotheses. -/
meta def simp_using_hs (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (cfg : simp_config := {}) : smt_tactic unit :=
@ -239,7 +239,7 @@ meta def simph (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list)
simp_using_hs hs attr_names ids cfg
meta def dsimp (es : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) : smt_tactic unit :=
tactic.interactive.dsimp es attr_names ids []
tactic.interactive.dsimp es attr_names ids (loc.ns [])
meta def rsimp : smt_tactic unit :=
do ccs ← to_cc_state, _root_.rsimp.rsimplify_goal ccs