def internal_append_nil

bend-mathlib@0.8.1.0 · string.bend:11

import bend-mathlib@0.8.1.0/string.bend as String

import Base

11def internal_append_nil(a: String) -> {a == String.append(a, SNil{}) : String}:
12  match a:
13    case SNil{}:
14      {==}
15    case SCon{+h, +t}:
16      %internal_append_nil(t) : {SCon{h, t} == SCon{h, _} : String}
17      {==}

Uses (2)

Used by (2)