erg/tests/should_ok/dependent_refinement.er
2024-09-15 01:20:10 +09:00

13 lines
301 B
Python

ndarray = pyimport "ndarray"
a as ndarray.NDArray(Int, [2, 3]) = todo()
check|T, Shape: {A: [Nat; _] | all(map((X -> X > 1), A))}|(
_: ndarray.NDArray(T, Shape)
) = None
check a
check2|T, Shape: [Nat; _]|(
_: {_: ndarray.NDArray(T, Shape) | all(map((X -> X > 1), Shape))}
) = None
check2 a