michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore(library/init/nat): replace 'no_confusion' with 'by contradiction'

Browse source
This commit is contained in:
Leonardo de Moura 2015-04-30 21:26:52 -07:00
parent 2d9c950144
commit 1e18a76bdb
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/nat.lean
View file

@ -31,8 +31,8 @@ namespace nat
protected definition has_decidable_eq [instance] : ∀ x y : nat, decidable (x = y)
| has_decidable_eq zero zero := inl rfl
| has_decidable_eq (succ x) zero := inr (λ h, nat.no_confusion h)
| has_decidable_eq zero (succ y) := inr (λ h, nat.no_confusion h)
| has_decidable_eq (succ x) zero := inr (by contradiction)
| has_decidable_eq zero (succ y) := inr (by contradiction)
| has_decidable_eq (succ x) (succ y) :=
if H : x = y
then inl (eq.rec_on H rfl)