conjure icon indicating copy to clipboard operation
conjure copied to clipboard

Error checking is matrix is in set of sequence

Open ChrisJefferson opened this issue 2 years ago • 0 comments

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) )

ChrisJefferson avatar Apr 06 '22 15:04 ChrisJefferson