def app_assoc

mylsm-lsm-store@0.3.2.0 · src/Wal.bend:220

import Base

220def app_assoc(sa: String, sb: String, sc: String) -> {((sa ++ sb) ++ sc) == (sa ++ (sb ++ sc)) : String}:
221  match sa:
222    case SNil{}:
223      {==}
224    case SCon{h, t}:
225      %app_assoc(t, sb, sc) : {SCon{h, (t ++ sb) ++ sc} == SCon{h, _} : String}
226      {==}