From 19596eae778bdc08ffef1e54448e905b71a4da3c Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Mon, 21 Nov 2016 09:11:22 -0800 Subject: [PATCH] fix(library/init/logic.lean): if_true and if_false take instance as implicit instead of inst_implicit --- library/init/logic.lean | 4 ++-- tests/lean/run/simp_if_true_false.lean | 2 ++ 2 files changed, 4 insertions(+), 2 deletions(-) create mode 100644 tests/lean/run/simp_if_true_false.lean diff --git a/library/init/logic.lean b/library/init/logic.lean index f2bb257c8e..26706e3e47 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -817,11 +817,11 @@ lemma if_simp_congr {α : Type u} {b c : Prop} [dec_b : decidable b] {x y u v : @if_ctx_simp_congr α b c dec_b x y u v h_c (λ h, h_t) (λ h, h_e) @[simp] -def if_true {α : Type u} (t e : α) : (if true then t else e) = t := +def if_true {α : Type u} {h : decidable true} (t e : α) : (@ite true h α t e) = t := if_pos trivial @[simp] -def if_false {α : Type u} (t e : α) : (if false then t else e) = e := +def if_false {α : Type u} {h : decidable false} (t e : α) : (@ite false h α t e) = e := if_neg not_false lemma if_ctx_congr_prop {b c x y u v : Prop} [dec_b : decidable b] [dec_c : decidable c] diff --git a/tests/lean/run/simp_if_true_false.lean b/tests/lean/run/simp_if_true_false.lean new file mode 100644 index 0000000000..fba9dd22bd --- /dev/null +++ b/tests/lean/run/simp_if_true_false.lean @@ -0,0 +1,2 @@ +example (m n p : ℕ) : ite (m = m) n p = n := by simp +example (m n p : ℕ) : ite (m ≠ m) n p = p := by simp