def rev_rr

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

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

import Base

500def rev_rr(-A: Data, xs: List<&2, A>, acc: List<&2, A>, b: List<&2, A>) -> {List.reverse.go(&2, A, List.reverse.go(&2, A, xs, acc), b) == List.reverse.go(&2, A, acc, List.append(&2, A, xs, b)) : List<&2, A>}:
501  match xs:
502    case Nil{}:
503      {==}
504    case Con{h, t}:
505      rev_rr(A, t, Con{h, acc}, b)

Uses (3)

Used by (1)

bend-osdev-bpf@0.1.0.0/PROOF:rev_twice