def internal_reverse_reverse

bend-mathlib@0.8.1.0 · string.bend:110

import Base

110def internal_reverse_reverse(a: String) -> {a == String.reverse(String.reverse(a)) : String}:
111  match a:
112    case SNil{}:
113      {==}
114    case SCon{+h, +t}:
115      %internal_reverse_go_spec(t, SCon{h, SNil{}}) : {SCon{h, t} == String.reverse.go(_, SNil{}) : String}
116      %internal_reverse_append(String.reverse(t), SCon{h, SNil{}}) : {SCon{h, t} == _ : String}
117      %internal_reverse_reverse(t) : {SCon{h, t} == String.append(String.reverse(SCon{h, SNil{}}), _) : String}
118      {==}