diff options
| author | Brian Campbell | 2019-03-15 16:39:43 +0000 |
|---|---|---|
| committer | Brian Campbell | 2019-03-15 18:42:09 +0000 |
| commit | c1f9e24213b50fb622ac94f816e304eabc75ba75 (patch) | |
| tree | 11ee8b5ae1f4349879620241b729ea0ce653f96a /test/coq | |
| parent | d74ad78a26a92c054b93e4fdce9623d0fdca7edd (diff) | |
Add coq test case for for-loop type variable
Diffstat (limited to 'test/coq')
| -rw-r--r-- | test/coq/_CoqProject | 2 | ||||
| -rw-r--r-- | test/coq/pass/foreach_using_tyvar.sail | 11 |
2 files changed, 13 insertions, 0 deletions
diff --git a/test/coq/_CoqProject b/test/coq/_CoqProject new file mode 100644 index 00000000..a694372c --- /dev/null +++ b/test/coq/_CoqProject @@ -0,0 +1,2 @@ +-R ../../../bbv/theories bbv +-R ../../lib/coq/ Sail diff --git a/test/coq/pass/foreach_using_tyvar.sail b/test/coq/pass/foreach_using_tyvar.sail new file mode 100644 index 00000000..8aabe00c --- /dev/null +++ b/test/coq/pass/foreach_using_tyvar.sail @@ -0,0 +1,11 @@ +$include <arith.sail> + +val f : forall 'n, 'n != 5. int('n) -> unit + +val magic : forall 'n. int('n) -> bool effect {rreg} + +val g : int -> unit effect {rreg} + +function g(x) = + foreach (n from 0 to x) + if n != 5 & magic(n) then f(n) |