ToNat Type Class

This file defines the ToNat type class for converting values to natural numbers. This provides a uniform interface for extracting natural number representations from various types in the CNat hierarchy.

class ToNat (α : Type u) : Type u

Type class for converting values to natural numbers.

• toNat : α → ℕ

  Convert a value to a natural number.

instance instToNatNat : ToNat ℕ

Equations

• instToNatNat = { toNat := id }

instance instCoeHeadNatOfToNat {α : Type u} [ToNat α] : CoeHead α ℕ

Equations

• instCoeHeadNatOfToNat = { coe := ToNat.toNat }

class LawfulToNat (α : Type u) [ToNat α] [Zero α] [HasSucc α] : Prop

A ToNat instance on a type α having zero and successor is lawful if toNat maps zero to zero and commutes with successor.

• toNat_zero : ToNat.toNat 0 = 0
• toNat_succ (n : α) : ToNat.toNat (succ' n) = ToNat.toNat n + 1

instance instLawfulToNatNat : LawfulToNat ℕ