~/jendhub

def AP.new_eq

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

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

1157def AP.new_eq(-T: Data, +d: Nat, +v: T) -> {Array.new(T, d, v) == AP.build(T, AP.tnew(T, d, v)) : Array<T>}:
1158  match d:
1159    case 0n:
1160      {==}
1161    case 1n+p:
1162      %Equal.sym(Array<T>, Array.new(T, p, v), AP.build(T, AP.tnew(T, p, v)), AP.new_eq(T, p, v)) : {ANode{_, _} == ANode{AP.build(T, AP.tnew(T, p, v)), AP.build(T, AP.tnew(T, p, v))} : Array<T>}
1163      {==}

Uses (6)

Used by (3)