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

chore: arguments occurring in the lhs should be marked as implicit

Browse source
This commit is contained in:
Leonardo de Moura 2021-02-13 12:00:31 -08:00
parent 95183e4e60
commit 1a4eaa2418
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/SimpLemmas.lean
View file

@ -36,7 +36,7 @@ theorem forallCongr {α : Sort u} {p q : α → Prop} (h : ∀ a, (p a = q a)) :
this ▸ rfl
@[congr]
theorem iteCongr {x y u v : α} [s : Decidable b] [Decidable c] (h₁ : b = c) (h₂ : c → x = u) (h₃ : ¬ c → y = v) : ite b x y = ite c u v := by
theorem iteCongr {x y u v : α} {s : Decidable b} [Decidable c] (h₁ : b = c) (h₂ : c → x = u) (h₃ : ¬ c → y = v) : ite b x y = ite c u v := by
cases Decidable.em c with
| inl h => rw [ifPos h]; subst b; rw[ifPos h]; exact h₂ h
| inr h => rw [ifNeg h]; subst b; rw[ifNeg h]; exact h₃ h
@ -48,7 +48,7 @@ theorem Eq.mprNot {p q : Prop} (h₁ : p = q) (h₂ : ¬q) : ¬p :=
h₁ ▸ h₂
@[congr]
theorem diteCongr [s : Decidable b] [Decidable c]
theorem diteCongr {s : Decidable b} [Decidable c]
{x : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α}
(h₁ : b = c)
(h₂ : (h : c) → x (Eq.mprProp h₁ h) = u h)