Structures · Lean core

OfNat

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) : α).

Defined in: Init.Prelude
Shape: 2 explicit arguments · adds ofNat

Open in Mathlib docs

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by3

Forgetful instances

Every OfNat is also a

Provided automatically by

Concrete types that are instances59

Int
Nat
Rat
TopCat.carrier
BitVec
UInt64
UInt8
UInt16
UInt32
USize
Int32
Int8
Int64
Int16
PNat
ISize
PosNum
String.Pos.Raw
Dyadic
Float
OrderType
Float32
ONote
Lean.Grind.Ring.OfSemiring.Q
Std.Time.Month.Offset
Std.Time.Week.Offset
Std.Time.Second.Offset
Std.Time.Minute.Offset
Std.Time.Nanosecond.Offset
Std.Time.Day.Offset
Std.Time.Hour.Offset
Lean.JsonNumber
Lean.Level
Std.Time.Internal.UnitVal
Std.Time.Millisecond.Offset
Std.Time.Year.Offset
Std.Time.Duration
Std.Time.Timestamp
Std.Time.WallTime
Aesop.Nanos
Lean.JsonRpc.RequestID
Lean.Json
Lean.LeanOptionValue
Std.Time.Second.Ordinal
Std.Time.Day.Ordinal.OfYear
Std.Time.Week.OfYear.Ordinal
Std.Time.Nanosecond.Ordinal
Std.Time.Millisecond.Ordinal
Std.Time.Hour.Ordinal
Std.Time.Day.Ordinal
Std.Time.Minute.Ordinal
Std.Time.Month.Ordinal
Std.Time.Month.Quarter
Std.Time.Weekday.Ordinal
Std.Time.Week.Ordinal
Std.Time.Week.Aligned.Ordinal
Std.Time.Internal.Bounded.LE
Fin
Id

How is a type an instance?

Loading the hierarchy index…