mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-17 13:01:31 +03:00
9346db2d0c
See #66 for more discussion. Basically we don't want the type of `it` to be different for unsat or sat results, so we put undefined values in there instead. Also, instead of using tuples and different field names to distinguish formula arguments of various arities, we use a convention of fields `arg1`, `arg2`, ...
33 lines
780 B
Plaintext
33 lines
780 B
Plaintext
Loading module Cryptol
|
|
Q.E.D.
|
|
it : {result : Bit, arg1 : [4]}
|
|
|
|
Run-time error: no counterexample available
|
|
True
|
|
f 0 = False
|
|
it : {result : Bit, arg1 : [4]}
|
|
{result = False, arg1 = 0}
|
|
False
|
|
f 3 = True
|
|
it : {result : Bit, arg1 : [4]}
|
|
{result = True, arg1 = 3}
|
|
True
|
|
Unsatisfiable.
|
|
it : {result : Bit, arg1 : [4]}
|
|
|
|
Run-time error: no satisfying assignment available
|
|
g {x = 0, y = 1} = False
|
|
it : {result : Bit, arg1 : {x : [32], y : [32]}}
|
|
{result = False, arg1 = {x = 0, y = 1}}
|
|
g {x = 0, y = 0} = True
|
|
it : {result : Bit, arg1 : {x : [32], y : [32]}}
|
|
{result = True, arg1 = {x = 0, y = 0}}
|
|
h 0 0 = False
|
|
it : {result : Bit, arg1 : [8], arg2 : [8]}
|
|
{result = False, arg1 = 0, arg2 = 0}
|
|
0
|
|
0
|
|
h 0 1 = True
|
|
it : {result : Bit, arg1 : [8], arg2 : [8]}
|
|
{result = True, arg1 = 0, arg2 = 1}
|