diff options
| author | Brian Campbell | 2018-06-11 18:12:15 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-06-12 11:58:42 +0100 |
| commit | 9f63777bdf850b5c055c3b5040bb69cc779cdf3e (patch) | |
| tree | 14084747911c6496d3ca3a011cb64a0328aa4850 /test/coq | |
| parent | 59e94cd92f7c232be7b9147202514f95c08ff459 (diff) | |
Coq: support for range type, along with related existential improvements
Plus
- Complete solver support for inequalities
- Reduce exponentials in solver
Diffstat (limited to 'test/coq')
| -rw-r--r-- | test/coq/pass/rangetest.sail | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/test/coq/pass/rangetest.sail b/test/coq/pass/rangetest.sail new file mode 100644 index 00000000..d526d7aa --- /dev/null +++ b/test/coq/pass/rangetest.sail @@ -0,0 +1,9 @@ +$include <prelude.sail> + +val test : (range(2,3), range(1,8)) -> {'n, 'n <= 13. atom('n)} + +function test(x,y) = { + let z : range(3,11) = x + y; + let w : range(-6,2) = x - y; + z + w +}
\ No newline at end of file |