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

fix(library/init/data/nat/basic): tail recursive nat.repeat

Browse source
This commit is contained in:
Leonardo de Moura 2019-02-08 11:00:48 -08:00
parent 4339afc802
commit afc2569f7c
1 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
library/init/data/nat/basic.lean
View file

@ -77,9 +77,12 @@ instance : has_sub nat :=
instance : has_mul nat :=
⟨nat.mul⟩
@[specialize] def {u} repeat {α : Type u} (f : nat → α → α) : nat → α → α
| 0 m := m
| (succ n) m := f n (repeat n m)
@[specialize] def {u} repeat_core {α : Type u} (f : nat → α → α) (s : nat) : nat → α → α
| 0 a := a
| (succ n) a := repeat_core n (f (s - (succ n)) a)
@[inline] def {u} repeat {α : Type u} (f : nat → α → α) (n : nat) (a : α) : α :=
repeat_core f n n a
protected def pow (m : nat) : nat → nat
| 0 := 1