~/jendhub

def mirror.node

lawful-arrays@0.1.0.0 · proof_tree.bend:42

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

42def mirror.node(-T: Data, -xs: Array<T>, -ys: Array<T>, m1: Mirror(T, xs), m2: Mirror(T, ys))
43  -> Mirror(T, ANode{xs, ys}):
44  (t1, e1) = m1
45  (t2, e2) = m2
46  (TNode{t1, t2}, anode_eq(T, fromT(T, t1), fromT(T, t2), xs, ys, e1, e2))

Uses (6)

Used by (1)