@[instance_reducible]

instance instZeroString_provenance : Zero String

Equations

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

@[instance_reducible]

instance instAddString_provenance : Add String

Equations

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

@[instance_reducible]

instance instSubString_provenance : Sub String

Equations

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

@[instance_reducible]

instance instMulString_provenance : Mul String

Equations

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

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

@[instance_reducible]

instance instValueTypeString : ValueType String

Equations

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

Home · Documentation · Publications · Contributors · Source · Cite