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

chore(library/data/nat/decl): remove leftover

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-30 15:10:10 -08:00
parent dad94eafbe
commit 7dc055cfc9
1 changed files with 0 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/data/nat/decl.lean
View file

@ -147,10 +147,6 @@ namespace nat
definition le.is_decidable_rel [instance] : decidable_rel le :=
λ a b, decidable_iff_equiv _ (iff.intro le.of_eq_or_lt eq_or_lt_of_le)
inductive le2 (a : nat) : nat → Prop :=
refl : le2 a a,
of_lt : ∀ {b}, lt a b → le2 a b
definition le.rec_on {a : nat} {P : nat → Prop} {b : nat} (H : a ≤ b) (H₁ : P a) (H₂ : ∀ b, a < b → P b) : P b :=
begin
cases H with (b', hlt),