def internal_reverse_go_spec
bend-mathlib@0.8.1.0 · string.bend:70
import bend-mathlib@0.8.1.0/string.bend as String
import Base
70def internal_reverse_go_spec(s: String, +acc: String) -> {String.append(String.reverse(s), acc) == String.reverse.go(s, acc) : String}:
71 match s:
72 case SNil{}:
73 {==}
74 case SCon{+h, +t}:
75 %internal_reverse_go_spec(t, SCon{h, SNil{}}) : {String.append(_, acc) == String.reverse.go(t, SCon{h, acc}) : String}
76 %internal_append_assoc(String.reverse(t), SCon{h, SNil{}}, acc) : {_ == String.reverse.go(t, SCon{h, acc}) : String}
77 %internal_reverse_go_spec(t, SCon{h, acc}) : {String.append(String.reverse(t), SCon{h, acc}) == _ : String}
78 {==}