List from repeated elements?

Stream: new members

[R Dong]

I tried looking at the List documentation in the manual (there is none) and the list of autocompletion from VSCode, but I can't find how to create a list from repeated elements. By which I mean something like repeat a 5 giving [a, a, a, a, a]. How do I do this in Lean? Do I have to write the function myself?

[Michael Stoll]

docs#List.replicate ?

[R Dong]

Thanks, I didn't look at the mathlib docs

[R Dong]

BTW, is Nat and \N two different types?

[Julian Berman]

(Those are really the Lean core docs, they're just built and shown as part of the Mathlib docs, presumably until the Language Reference subsumes them as a better place to look.)

[Julian Berman]

\N is notation defined in Mathlib for Nat.

[Michael Stoll]

import Mathlib.Data.Nat.Notation

#check ℕ

[Julian Berman]

(wrong)

[Julian Berman]

Ah wait no, they're not the same. Never mind.

[Michael Stoll]

docs#Fin.repeat

[R Dong]

example f (n : ℕ) : List ℕ := List.replicate n 42
failed to synthesize
  OfNat ℕ 42
numerals are polymorphic in Lean, but the numeral `42` cannot be used in a context where the expected type is
  ℕ
due to the absence of the instance above
Additional diagnostic information may be available using the `set_option diagnostics true` command.

[Michael Stoll]

You need to import Mathlib.Data.Nat.Notation at the very least.

[R Dong]

Ok

[R Dong]

Hmmm, unknown module Mathlib

[Michael Stoll]

See here.

[R Dong]

I didn't run lake update