OfNat.{u} (α : Type u) : Nat → Type u

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	:	α
		The OfNat.ofNat function is automatically inserted by the parser when the user writes a numeric literal like 1 : α. Implementations of this typeclass can therefore customize the behavior of n : α based on n and α.

OfScientific.{u} (α : Type u) : Type u

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`.
[term,*]

term ::= ...
    | #[term,*]