← Copula mathematical handbook

@[instance_reducible]

instance Char.instUpwardEnumerable : Std.PRange.UpwardEnumerable Char

Equations

• Char.instUpwardEnumerable = { succ? := Char.succ?, succMany? := Char.succMany? }

@[simp]

theorem Char.pRangeSucc?_eq : Std.PRange.succ? = succ?

@[simp]

theorem Char.pRangeSuccMany?_eq : Std.PRange.succMany? = succMany?

@[instance_reducible]

instance Char.instHasSize : Std.Rxc.HasSize Char

Equations

• Char.instHasSize = { size := fun (lo hi : Char) => Std.Rxc.HasSize.size lo.ordinal hi.ordinal }

@[instance_reducible]

instance Char.instHasSize_1 : Std.Rxo.HasSize Char

Equations

• Char.instHasSize_1 = { size := fun (lo hi : Char) => Std.Rxo.HasSize.size lo.ordinal hi.ordinal }

@[instance_reducible]

instance Char.instHasSize_2 : Std.Rxi.HasSize Char

Equations

• Char.instHasSize_2 = { size := fun (hi : Char) => Std.Rxi.HasSize.size hi.ordinal }

@[instance_reducible]

instance Char.instLeast? : Std.PRange.Least? Char

Equations

• Char.instLeast? = { least? := some '\x00' }

@[simp]

theorem Char.least?_eq : Std.PRange.least? = some '\x00'

instance Char.instLawfulUpwardEnumerable : Std.PRange.LawfulUpwardEnumerable Char

instance Char.instLawfulUpwardEnumerableLE : Std.PRange.LawfulUpwardEnumerableLE Char

instance Char.instLawfulUpwardEnumerableLT : Std.PRange.LawfulUpwardEnumerableLT Char

instance Char.instLawfulUpwardEnumerableLeast? : Std.PRange.LawfulUpwardEnumerableLeast? Char

instance Char.instLawfulHasSize : Std.Rxc.LawfulHasSize Char

instance Char.instIsAlwaysFinite : Std.Rxc.IsAlwaysFinite Char

instance Char.instLawfulHasSize_1 : Std.Rxo.LawfulHasSize Char

instance Char.instIsAlwaysFinite_1 : Std.Rxo.IsAlwaysFinite Char

instance Char.instLawfulHasSize_2 : Std.Rxi.LawfulHasSize Char

instance Char.instIsAlwaysFinite_2 : Std.Rxi.IsAlwaysFinite Char