def app_nilu

bend-osdev-bytes@0.1.1.0 · PROOF.bend:248

import bend-osdev-bytes@0.1.1.0/PROOF.bend as PROOF

import Base

248def app_nilu(+xs: List<&2, U32>) -> {List.append(&2, U32, xs, Nil{}) == xs : List<&2, U32>}:
249  match xs:
250    case Nil{}:
251      {==}
252    case Con{h, t}:
253      Equal.cong(List<&2, U32>, List<&2, U32>, l => Con{h, l}, List.append(&2, U32, t, Nil{}), t, app_nilu(t))

Uses (4)

Used by (4)