mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-17 04:44:39 +03:00
1cf61e12c3
Per @weaversa's suggestions in #66, we now bind records to `it` for sat results, leading to less ambiguity about the meaning of those results. There is still some weirdness to this; the fields present in the record change based on the result and the arity of the formula, but this seems like a reasonable approach given that it's not an expression that needs a type.
26 lines
644 B
Plaintext
26 lines
644 B
Plaintext
Loading module Cryptol
|
|
Q.E.D.
|
|
it : {result : Bit}
|
|
{result = True}
|
|
f 0 = False
|
|
it : {result : Bit, arg : [4]}
|
|
{result = False, arg = 0}
|
|
f 3 = True
|
|
it : {result : Bit, arg : [4]}
|
|
{result = True, arg = 3}
|
|
Unsatisfiable.
|
|
it : {result : Bit}
|
|
{result = False}
|
|
g {x = 0, y = 1} = False
|
|
it : {result : Bit, arg : {x : [32], y : [32]}}
|
|
{result = False, arg = {x = 0, y = 1}}
|
|
g {x = 0, y = 0} = True
|
|
it : {result : Bit, arg : {x : [32], y : [32]}}
|
|
{result = True, arg = {x = 0, y = 0}}
|
|
h 0 0 = False
|
|
it : {result : Bit, args : ([8], [8])}
|
|
{result = False, args = (0, 0)}
|
|
h 0 1 = True
|
|
it : {result : Bit, args : ([8], [8])}
|
|
{result = True, args = (0, 1)}
|