Closed jwaldmann closed 10 years ago
data Unit = Unit
works for me. But you might get a rather unintuitive output from CO4 when the unknown value is of type Unit
:
data Bool = False | True
data Unit = Unit
constraint x = case x of
Unit -> True
gives
Start producing CNF
Known result: valid
Abort due to known result
No solution found
Nothing
The second line states that the constraint is valid, i.e. it's satisfied for all x
. As CO4 notes this during abstract evaluation, the SAT solver is not run, but gives the misleading message No solution found
.
it seems that currently the type
()
is not supported