~/bend-docscommunity

string.bend checks

raw source on the hub · import bend-mathlib@0.6.0.0/string.bend as MString

bend-mathlib/string.bend: String append, reverse and length, and comparison. Comparison descends String.eq -> String.cmp -> Char.cmp -> U32.cmp -> Word.cmp.

2 imports
import Base
import ./bool.bend as MBool

Laws

law append_nil provedsource · line 19 · raw

@a:String -> {String.append(a, "") == a : String}

The empty string is a right identity for append: a ++ "" = a.

law nil_append provedsource · line 27 · raw

@-a:String -> {String.append("", a) == a : String}

The empty string is a left identity for append: "" ++ a = a.

law append_assoc provedsource · line 43 · raw

@a:String -> @-b:String -> @-c:String -> {String.append(String.append(a, b), c) == String.append(a, String.append(b, c)) : String}

Append is associative: (a ++ b) ++ c = a ++ (b ++ c).

law length_append provedsource · line 61 · raw

@a:String -> @-b:String -> {String.length(String.append(a, b)) == Nat.add(String.length(a), String.length(b)) : Nat}

The length of an append is the sum of the lengths.

law reverse_go_spec provedsource · line 80 · raw

@s:String -> @acc:String -> {String.reverse.go(s, acc) == String.append(String.reverse(s), acc) : String}

The reverse accumulator loop appends the reversed string to the accumulator.

law reverse_append provedsource · line 101 · raw

@a:String -> @b:String -> {String.reverse(String.append(a, b)) == String.append(String.reverse(b), String.reverse(a)) : String}

Reversing an append reverses and swaps the parts: reverse (a ++ b) = reverse b ++ reverse a.

law reverse_reverse provedsource · line 120 · raw

@a:String -> {String.reverse(String.reverse(a)) == a : String}

Reversing twice gives the string back.

law u32_cmp_refl provedsource · line 145 · raw

@x:U32 -> {U32.cmp(x, x) == EQ{} : Cmp}

Comparing a U32 with itself gives EQ.

law char_cmp_refl provedsource · line 159 · raw

@c:Char -> {Char.cmp(c, c) == ((c, c), EQ{}) : Pair(Pair(Char, Char), Cmp)}

Comparing a character with itself gives EQ and hands both back.

law cmp_refl provedsource · line 178 · raw

@s:String -> {String.cmp(s, s) == ((s, s), EQ{}) : Pair(Pair(String, String), Cmp)}

Comparing a string with itself gives EQ and hands both back.

law eq_refl provedsource · line 186 · raw

@s:String -> {String.eq(s, s) == True{} : Bool}

Every string is equal to itself under String.eq.

law u32_eq_of_is_eq provedsource · line 226 · raw

@a:U32 -> @b:U32 -> @h:{U32.is_eq(a, b) == True{} : Bool} -> {a == b : U32}

Two U32s that U32.is_eq calls equal are equal.

law char_eq_of_is_eq provedsource · line 239 · raw

@a:Char -> @b:Char -> @h:{Char.is_eq(a, b) == True{} : Bool} -> {a == b : Char}

Two characters that Char.is_eq calls equal are equal.

law eq_of_eq_true provedsource · line 272 · raw

@a:String -> @b:String -> @h:{String.eq(a, b) == True{} : Bool} -> {a == b : String}

Two strings that String.eq calls equal are equal.

law append_nil_sym provedsource · line 292 · raw

@a:String -> {a == String.append(a, "") : String}

The empty string is a right identity for append: a ++ "" = a, reversed to rewrite toward the simple side.

law nil_append_sym provedsource · line 300 · raw

@-a:String -> {a == String.append("", a) : String}

The empty string is a left identity for append: "" ++ a = a, reversed to rewrite toward the simple side.

law append_assoc_sym provedsource · line 308 · raw

@a:String -> @-b:String -> @-c:String -> {String.append(a, String.append(b, c)) == String.append(String.append(a, b), c) : String}

Append is associative: (a ++ b) ++ c = a ++ (b ++ c), reversed to rewrite toward the simple side.

law length_append_sym provedsource · line 318 · raw

@a:String -> @-b:String -> {Nat.add(String.length(a), String.length(b)) == String.length(String.append(a, b)) : Nat}

The length of an append is the sum of the lengths, reversed to rewrite toward the simple side.

law reverse_go_spec_sym provedsource · line 327 · raw

@s:String -> @acc:String -> {String.append(String.reverse(s), acc) == String.reverse.go(s, acc) : String}

The reverse accumulator loop appends the reversed string to the accumulator, reversed to rewrite toward the simple side.

law reverse_append_sym provedsource · line 336 · raw

@a:String -> @b:String -> {String.append(String.reverse(b), String.reverse(a)) == String.reverse(String.append(a, b)) : String}

Reversing an append reverses and swaps the parts: reverse (a ++ b) = reverse b ++ reverse a, reversed to rewrite toward the simple side.

law reverse_reverse_sym provedsource · line 345 · raw

@a:String -> {a == String.reverse(String.reverse(a)) : String}

Reversing twice gives the string back, reversed to rewrite toward the simple side.

law u32_cmp_refl_sym provedsource · line 353 · raw

@x:U32 -> {EQ{} == U32.cmp(x, x) : Cmp}

Comparing a U32 with itself gives EQ, reversed to rewrite toward the simple side.

law char_cmp_refl_sym provedsource · line 361 · raw

@c:Char -> {((c, c), EQ{}) == Char.cmp(c, c) : Pair(Pair(Char, Char), Cmp)}

Comparing a character with itself gives EQ and hands both back, reversed to rewrite toward the simple side.

law cmp_refl_sym provedsource · line 369 · raw

@s:String -> {((s, s), EQ{}) == String.cmp(s, s) : Pair(Pair(String, String), Cmp)}

Comparing a string with itself gives EQ and hands both back, reversed to rewrite toward the simple side.

law eq_refl_sym provedsource · line 377 · raw

@s:String -> {True{} == String.eq(s, s) : Bool}

Every string is equal to itself under String.eq, reversed to rewrite toward the simple side.

Definitions

def internal_false_ne_true source · line 6 · raw

@e:{False{} == True{} : Bool} -> Empty

def internal_append_nil source · line 10 · raw

@a:String -> {a == String.append(a, "") : String}

def internal_append_assoc source · line 34 · raw

@a:String -> @-b:String -> @-c:String -> {String.append(a, String.append(b, c)) == String.append(String.append(a, b), c) : String}

def internal_length_append source · line 52 · raw

@a:String -> @-b:String -> {Nat.add(String.length(a), String.length(b)) == String.length(String.append(a, b)) : Nat}

def internal_reverse_go_spec source · line 69 · raw

@s:String -> @+acc:String -> {String.append(String.reverse(s), acc) == String.reverse.go(s, acc) : String}

def internal_reverse_append source · line 88 · raw

@a:String -> @+b:String -> {String.append(String.reverse(b), String.reverse(a)) == String.reverse(String.append(a, b)) : String}

def internal_reverse_reverse source · line 109 · raw

@a:String -> {a == String.reverse(String.reverse(a)) : String}

def internal_word_cmp_refl source · line 127 · raw

@n:Nat -> @w:Word(n) -> {EQ{} == Word.cmp(n, w, w) : Cmp}

def internal_u32_cmp_refl source · line 138 · raw

@x:U32 -> {EQ{} == U32.cmp(x, x) : Cmp}

def internal_char_cmp_refl source · line 152 · raw

@c:Char -> {((c, c), EQ{}) == Char.cmp(c, c) : Pair(Pair(Char, Char), Cmp)}

def internal_cmp_refl source · line 166 · raw

@s:String -> {((s, s), EQ{}) == String.cmp(s, s) : Pair(Pair(String, String), Cmp)}

def internal_fin_head source · line 194 · raw

@ab:Bool -> @bb:Bool -> @c:Cmp -> @h:{Cmp.is_eq(Word.cmp.fin(ab, bb, c)) == True{} : Bool} -> {ab == bb : Bool}

def internal_fin_tail source · line 203 · raw

@ab:Bool -> @bb:Bool -> @c:Cmp -> @h:{Cmp.is_eq(Word.cmp.fin(ab, bb, c)) == True{} : Bool} -> {Cmp.is_eq(c) == True{} : Bool}

def internal_word_eq source · line 212 · raw

@n:Nat -> @a:Word(n) -> @b:Word(n) -> @+h:{Cmp.is_eq(Word.cmp(n, a, b)) == True{} : Bool} -> {a == b : Word(n)}

def internal_rec_is_eq source · line 251 · raw

@h1:Char -> @h2:Char -> @rr:Pair(Pair(String, String), Cmp) -> {Cmp.is_eq(Pair.snd(Pair(String, String), Cmp, String.cmp.rec(h1, h2, rr))) == Cmp.is_eq(Pair.snd(Pair(String, String), Cmp, rr)) : Bool}

def internal_is_eq_of source · line 256 · raw

@c:Cmp -> @+d:Cmp -> @e:{c == d : Cmp} -> @h:{Cmp.is_eq(c) == True{} : Bool} -> {Cmp.is_eq(d) == True{} : Bool}

def internal_step source · line 260 · raw

@+x:U32 -> @+y:U32 -> @+t1:String -> @+t2:String -> @c:Cmp -> @ec:{c == U32.cmp(x, y) : Cmp} -> @h:{Cmp.is_eq(Pair.snd(Pair(String, String), Cmp, String.cmp.fin(t1, t2, ((Chr{x}, Chr{y}), c)))) == True{} : Bool} -> @ih:(@_:{String.eq(t1, t2) == True{} : Bool} -> {t1 == t2 : String}) -> {SCon{Chr{x}, t1} == SCon{Chr{y}, t2} : String}