Open SaadAttieh opened 5 years ago
Savile Row can't parse those question marks.
Yeah, I did think that wasn't eprime syntax. :P On 22 Jul 2019, at 1:42 pm, Peter Nightingale notifications@github.com wrote:
Savile Row can't parse those question marks.
— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub, or mute the thread.
@pwn1 - SR seems to assume that []
is the same as ([] : matrix indexed by [int()] of int)
So this is UNSAT (with or without the type annotation)
letting s be ([] : `matrix indexed by [int()] of int`)
find a : int(1..5)
such that a = s[1]
And this has 1 solution with the type annotation, and it is UNSAT without
letting s be ([] : `matrix indexed by [int()] of bool`)
find a : bool
such that
a = s[1]
OK, that should be documented I suppose.
Conjure output: