def app_nil

bend-osdev-bpf@0.1.0.0 · PROOF.bend:507

import bend-osdev-bpf@0.1.0.0/PROOF.bend as PROOF

import Base

507def app_nil(-A: Data, +xs: List<&2, A>) -> {List.append(&2, A, xs, Nil{}) == xs : List<&2, A>}:
508  match xs:
509    case Nil{}:
510      {==}
511    case Con{h, t}:
512      Equal.cong(List<&2, A>, List<&2, A>, l => Con{h, l}, List.append(&2, A, t, Nil{}), t, app_nil(A, t))

Uses (3)

Used by (1)

bend-osdev-bpf@0.1.0.0/PROOF:rev_twice