~/jendhub

def get_pair.go

lawful-arrays@0.1.0.0 · PROOF.bend:78

import lawful-arrays@0.1.0.0/PROOF.bend as PROOF
import Base
import lawful-arrays@0.1.0.0/proof_tree.bend as P

78def get_pair.go(-T: Data, -a: Array<T>, +i: U32, m: P.Mirror(T, a)) ->
79  {Array.get(T, a, i) == (a, Pair.snd(Array<T>, T, Array.get(T, a, i))) : Array<T> & T}:
80  (t, e) = m
81  %e : {Array.get(T, _, i) == (_, Pair.snd(Array<T>, T, Array.get(T, _, i))) : Array<T> & T}
82  P.get_pair_t(T, t, i)

Uses (8)

Used by (1)