@[implicit_reducible]

instance instZeroString_provenance : Zero String

Equations

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

@[implicit_reducible]

instance instAddString_provenance : Add String

Equations

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

@[implicit_reducible]

instance instSubString_provenance : Sub String

Equations

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

@[implicit_reducible]

instance instMulString_provenance : Mul String

Equations

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

Bridging String.foldl / String.Slice.foldl to List.foldl

In Lean 4.29 String.foldl is defined through String.Slice.foldl, which itself is Std.Iter.fold over the iterator of characters. We restate it as a List.foldl on toList to reuse standard list-induction arguments.

Nat.repr n has no underscores: parsing reduces to digit folds

Tracking the four-tuple state of String.Slice.isNat

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

@[implicit_reducible]

instance instValueTypeString : ValueType String

Equations

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

Home · Documentation · Publications · Contributors · Source · Cite