diff options
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) |