def internal_length_reverse_go

bend-mathlib@0.8.1.0 · string.bend:354

import Base
import bend-mathlib@0.8.1.0/nat.bend as MNat

354def internal_length_reverse_go(s: String, -acc: String) -> {Nat.add(String.length(s), String.length(acc)) == String.length(String.reverse.go(s, acc)) : Nat}:
355  match s:
356    case SNil{}:
357      {==}
358    case SCon{h, +t}:
359      %MNat.add_succ(String.length(t), String.length(acc)) : {_ == String.length(String.reverse.go(t, SCon{h, acc})) : Nat}
360      internal_length_reverse_go(t, SCon{h, acc})