def clone

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/array.bend:324

import Base

324def clone(-T: Data, +t: Tree<T>) -> {Array.clone(T, thaw(T, t)) == (thaw(T, t), thaw(T, t)) : Array<T> & Array<T>}:
325  match t:
326    case TLeaf{x}:
327      {==}
328    case TNode{+l, +r}:
329      %Equal.sym(Array<T> & Array<T>, Array.clone(T, thaw(T, l)), (thaw(T, l), thaw(T, l)), clone(T, l)) : {Array.clone.node(T, _, Array.clone(T, thaw(T, r))) == (ANode{thaw(T, l), thaw(T, r)}, ANode{thaw(T, l), thaw(T, r)}) : Array<T> & Array<T>}
330      %Equal.sym(Array<T> & Array<T>, Array.clone(T, thaw(T, r)), (thaw(T, r), thaw(T, r)), clone(T, r)) : {Array.clone.node(T, (thaw(T, l), thaw(T, l)), _) == (ANode{thaw(T, l), thaw(T, r)}, ANode{thaw(T, l), thaw(T, r)}) : Array<T> & Array<T>}
331      {==}