instance instZeroString_provenance : Zero String

Equations

• instZeroString_provenance = { zero := Nat.repr 0 }

instance instAddString_provenance : Add String

Equations

• One or more equations did not get rendered due to their size.

instance instSubString_provenance : Sub String

Equations

• instSubString_provenance = { sub := fun (x x_1 : String) => "" }

instance instMulString_provenance : Mul String

Equations

• instMulString_provenance = { mul := fun (x x_1 : String) => "" }

theorem toNat_reprStr (n : ℕ) : n.repr.toNat? = some n

instance instValueTypeString : ValueType String

Equations

• One or more equations did not get rendered due to their size.