cryptol/tests/issues/issue066.icry

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
bind `it` even when no counterexample/sat is available; add tests Similar to what @weaversa requested in #66, we bind `it` to `False` when we can't find a sat assignment, and `it` to `True` when we've proved a theorem. Also adds some simple tests for the sat/prove result binding, and let binding at the repl. 2014-08-20 04:11:43 +04:00			`let f x = (x : [4]) == x`
			`:prove f`
			`:t it`
			`it`
Bind sat/prove results to a single type for both unsat and sat, use more record fields 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`, ... 2014-08-22 02:02:35 +04:00			`it.result`
bind `it` even when no counterexample/sat is available; add tests Similar to what @weaversa requested in #66, we bind `it` to `False` when we can't find a sat assignment, and `it` to `True` when we've proved a theorem. Also adds some simple tests for the sat/prove result binding, and let binding at the repl. 2014-08-20 04:11:43 +04:00			`let f x = (x : [4]) == 3`
			`:prove f`
			`:t it`
			`it`
Bind sat/prove results to a single type for both unsat and sat, use more record fields 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`, ... 2014-08-22 02:02:35 +04:00			`it.result`
bind `it` even when no counterexample/sat is available; add tests Similar to what @weaversa requested in #66, we bind `it` to `False` when we can't find a sat assignment, and `it` to `True` when we've proved a theorem. Also adds some simple tests for the sat/prove result binding, and let binding at the repl. 2014-08-20 04:11:43 +04:00			`:sat f`
			`:t it`
			`it`
Bind sat/prove results to a single type for both unsat and sat, use more record fields 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`, ... 2014-08-22 02:02:35 +04:00			`it.result`
bind `it` even when no counterexample/sat is available; add tests Similar to what @weaversa requested in #66, we bind `it` to `False` when we can't find a sat assignment, and `it` to `True` when we've proved a theorem. Also adds some simple tests for the sat/prove result binding, and let binding at the repl. 2014-08-20 04:11:43 +04:00			`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`
reword :sat and :prove results as records 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. 2014-08-21 04:10:40 +04:00			`it`
			`let h x y = (x : [8]) < y`
			`:prove h`
			`:t it`
			`it`
Bind sat/prove results to a single type for both unsat and sat, use more record fields 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`, ... 2014-08-22 02:02:35 +04:00			`let result = it`
			`result.arg1`
			`result.arg2`
reword :sat and :prove results as records 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. 2014-08-21 04:10:40 +04:00			`:sat h`
			`:t it`
bind `it` even when no counterexample/sat is available; add tests Similar to what @weaversa requested in #66, we bind `it` to `False` when we can't find a sat assignment, and `it` to `True` when we've proved a theorem. Also adds some simple tests for the sat/prove result binding, and let binding at the repl. 2014-08-20 04:11:43 +04:00			`it`