lean4-htt/library/init/data/string
Leonardo de Moura 49551036ed refactor(library/init): minor changes
Old `Nat.repeat` => `Nat.for`
Old `Nat.mrepeat` => `Nat.mfor`
New `Nat.repeat` has type
```
def repeat {α : Type u} (f : α → α) (n : Nat) (a : α) : α :=
``
`List.repeat` => `List.replicate` (like in Haskell)
Avoid weird `ℕ` in List library
2019-03-29 10:39:00 -07:00
..
basic.lean refactor(library/init): minor changes 2019-03-29 10:39:00 -07:00
default.lean chore(library): use lowercase in imports 2019-03-21 15:06:44 -07:00