def internal_append_assoc

bend-mathlib@0.8.1.0 · string.bend:35

import Base

35def internal_append_assoc(a: String, -b: String, -c: String) -> {String.append(a, String.append(b, c)) == String.append(String.append(a, b), c) : String}:
36  match a:
37    case SNil{}:
38      {==}
39    case SCon{+h, +t}:
40      %internal_append_assoc(t, b, c) : {SCon{h, String.append(t, String.append(b, c))} == SCon{h, _} : String}
41      {==}