def SizeW

lawful-arrays@0.1.0.0 · proof_shape.bend:10

import Base

10# Array.size(a) is (b, n) with b == a.
11def SizeW(-T: Type, -a: Array<T>) -> Type:
12  &b:Array<T> -> &n:U32 -> {Array.size(T, a) == (b, n) : Array<T> & U32} & {b == a : Array<T>}