Open bvssvni opened 4 years ago
The theorem prover can first evaluate even(add(1, 3))
and then look for [_, _ -> even]
which returns true
. Then it evaluates (even(1), even(3))
and finds the case (false, false)
.
It could be required to cover every type information with some test, and cover every test with some type information.
The ty [even] = eq
does not require checking this for every input of eq
, but only for some input.
This only requires evaluation and comparing results, but gives a stronger guarantee than dynamic types. In addition the type information can be used to e.g. reduce add[even]
to eq
.
Using
ty
syntax from https://github.com/PistonDevelopers/dyon/issues/636By extending
ty
with support for paths and a new keywordchk
, one can create a language that supports a subset of path semantics.For example:
This works because:
The output is compared to evaluating
even(add(1, 3))
.Another example:
Another example: