mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-17 04:44:39 +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`, ...
35 lines
363 B
Plaintext
35 lines
363 B
Plaintext
let f x = (x : [4]) == x
|
|
:prove f
|
|
:t it
|
|
it
|
|
it.result
|
|
let f x = (x : [4]) == 3
|
|
:prove f
|
|
:t it
|
|
it
|
|
it.result
|
|
:sat f
|
|
:t it
|
|
it
|
|
it.result
|
|
let f x = (x : [4]) == 3 && x == 2
|
|
:sat f
|
|
:t it
|
|
it
|
|
let g p = (p : { x : [32], y : [32]}).x == p.y
|
|
:prove g
|
|
:t it
|
|
it
|
|
:sat g
|
|
:t it
|
|
it
|
|
let h x y = (x : [8]) < y
|
|
:prove h
|
|
:t it
|
|
it
|
|
let result = it
|
|
result.arg1
|
|
result.arg2
|
|
:sat h
|
|
:t it
|
|
it |