conjure
conjure copied to clipboard
Error checking is matrix is in set of sequence
I'm not 100% sure this is even valid (I'm mixing sequences and matrices), but it tells me "this should never happen" :)
language Essence 1.3
find ixmat: set of sequence (size 5) of int(1..3)
find y : bool
such that
$ This works
( y = ([1,2,1,2,1] in ixmat) )
such that
$ This doesn't
forAll ix : matrix indexed by [int(1..5)] of int(1..3).
( y = (ix in ixmat) )