~/jendhub

def AP.get_app_r

bend-osdev-array@0.1.0.1 · PROOF.bend:837

import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF
import Base

837def AP.get_app_r(-T: Data, xs: List<&2, T>, -ys: List<&2, T>, -k: Nat) -> {List.get(&2, T, List.append(&2, T, xs, ys), Nat.add(List.length(&2, T, xs), k)) == List.get(&2, T, ys, k) : Maybe<&2, T>}:
838  match xs:
839    case Nil{}:
840      {==}
841    case Con{x, t}:
842      AP.get_app_r(T, t, ys, k)

Uses (7)

Used by (1)