The class OfNat α n powers the numeric literal parser. If you write 37 : α, Lean will attempt to synthesize OfNat α 37, and will generate the term (OfNat.ofNat 37 : α).

There is a bit of infinite regress here since the desugaring apparently still contains a literal 37 in it. The type of expressions contains a primitive constructor for "raw natural number literals", which you can directly access using the macro nat_lit 37. Raw number literals are always of type Nat. So it would be more correct to say that Lean looks for an instance of OfNat α (nat_lit 37), and it generates the term (OfNat.ofNat (nat_lit 37) : α).

Instance Constructor

OfNat.mk.{u}

Methods

ofNat : α

For decimal and scientific numbers (e.g., 1.23, 3.12e10). Examples:

• 1.23 is syntax for OfScientific.ofScientific (nat_lit 123) true (nat_lit 2)

• 121e100 is syntax for OfScientific.ofScientific (nat_lit 121) false (nat_lit 100)

Note the use of nat_lit; there is no wrapping OfNat.ofNat in the resulting term.

Instance Constructor

OfScientific.mk.{u}

Methods

ofScientific : Nat → Bool → Nat → α

term ::= ...
    | The syntax `[a, b, c]` is shorthand for `a :: b :: c :: []`, or
`List.cons a (List.cons b (List.cons c List.nil))`. It allows conveniently constructing
list literals.

For lists of length at least 64, an alternative desugaring strategy is used
which uses let bindings as intermediates as in
`let left := [d, e, f]; a :: b :: c :: left` to avoid creating very deep expressions.
Note that this changes the order of evaluation, although it should not be observable
unless you use side effecting operations like `dbg_trace`.


Conventions for notations in identifiers:

 * The recommended spelling of `[]` in identifiers is `nil`.

 * The recommended spelling of `[a]` in identifiers is `singleton`.[term,*]

term ::= ...
    | Syntax for `Array α`. 

Conventions for notations in identifiers:

 * The recommended spelling of `#[]` in identifiers is `empty`.

 * The recommended spelling of `#[x]` in identifiers is `singleton`.#[term,*]