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

chore(library/init/meta): use general when

Browse source
This commit is contained in:
Leonardo de Moura 2017-02-17 19:51:40 -08:00
parent 632c98aade
commit a9122a2c0a
2 changed files with 1 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/meta/smt/rsimp.lean
View file

@ -103,7 +103,7 @@ do t ← target,
try (replace_target new_t pr)
meta def rsimplify_at (ccs : cc_state) (h : expr) (m : option repr_map := none) : tactic unit :=
do tactic.when (expr.is_local_constant h = ff) (tactic.fail "tactic rsimplify_at failed, the given expression is not a hypothesis"),
do when (expr.is_local_constant h = ff) (tactic.fail "tactic rsimplify_at failed, the given expression is not a hypothesis"),
htype ← infer_type h,
(new_htype, heq) ← rsimplify ccs htype m,
try $ do assert (expr.local_pp_name h) new_htype,

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

@ -716,10 +716,6 @@ do g::gs ← get_goals,
meta instance : has_andthen (tactic unit) :=
⟨seq⟩
/- Applies tac if c holds -/
meta def when (c : Prop) [decidable c] (tac : tactic unit) : tactic unit :=
if c then tac else skip
meta constant is_trace_enabled_for : name → bool
/- Execute tac only if option trace.n is set to true. -/