def rev_app

bend-osdev-acpi@0.1.1.0 · PROOF_tables.bend:240

import bend-osdev-acpi@0.1.1.0/PROOF_tables.bend as PROOFTables

import Base

240def rev_app(-A: Data, +xs: List<&2, A>, +a: List<&2, A>, +b: List<&2, A>) -> {List.reverse.go(&2, A, a, List.append(&2, A, xs, b)) == List.reverse.go(&2, A, List.reverse.go(&2, A, xs, a), b) : List<&2, A>}:
241  match xs:
242    case Nil{}:
243      {==}
244    case Con{h, t}:
245      rev_app(A, t, Con{h, a}, b)

Uses (3)

Used by (1)

bend-osdev-acpi@0.1.1.0/PROOF_tables:revrev