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

fix(library/init/nat): recursor attribute should be in the top-level since nat was defined in the top-level

Browse source
This commit is contained in:
Leonardo de Moura 2016-04-28 16:34:37 -07:00
parent 5fc90adf6b
commit f05e52e59f
1 changed files with 7 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
library/init/nat.lean
View file

@ -10,15 +10,15 @@ open eq.ops decidable or
notation `ℕ` := nat
namespace nat
protected definition rec_on [reducible] [recursor] [unfold 2]
protected definition rec_on [reducible]
{C : ℕ → Type} (n : ℕ) (H₁ : C 0) (H₂ : Π (a : ℕ), C a → C (succ a)) : C n :=
nat.rec H₁ H₂ n
protected definition induction_on [recursor]
protected definition induction_on
{C : ℕ → Prop} (n : ℕ) (H₁ : C 0) (H₂ : Π (a : ℕ), C a → C (succ a)) : C n :=
nat.rec H₁ H₂ n
protected definition cases_on [reducible] [recursor] [unfold 2]
protected definition cases_on [reducible]
{C : ℕ → Type} (n : ℕ) (H₁ : C 0) (H₂ : Π (a : ℕ), C (succ a)) : C n :=
nat.rec H₁ (λ a ih, H₂ a) n
@ -271,3 +271,7 @@ namespace nat
theorem sub_lt_succ_iff_true [simp] (a b : ℕ) : a - b < succ a ↔ true :=
iff_true_intro !sub_lt_succ
end nat
attribute [recursor] nat.induction_on
attribute [recursor] [unfold 2] nat.cases_on
attribute [recursor] [unfold 2] nat.rec_on