From 743c689a1083f46e54d48e802d6e169e0df235b0 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Wed, 8 Jun 2022 13:42:00 -0700 Subject: [PATCH] Add a test for a type-level interface module --- tests/modsys/functors/T015.cry | 6 ++++++ tests/modsys/functors/T015.icry | 1 + tests/modsys/functors/T015.icry.stdout | 4 ++++ tests/modsys/functors/T015_S.cry | 7 +++++++ 4 files changed, 18 insertions(+) create mode 100644 tests/modsys/functors/T015.cry create mode 100644 tests/modsys/functors/T015.icry create mode 100644 tests/modsys/functors/T015.icry.stdout create mode 100644 tests/modsys/functors/T015_S.cry diff --git a/tests/modsys/functors/T015.cry b/tests/modsys/functors/T015.cry new file mode 100644 index 00000000..c9aa061a --- /dev/null +++ b/tests/modsys/functors/T015.cry @@ -0,0 +1,6 @@ + +submodule F where + import interface module T015_S + + x : n + x = 0 diff --git a/tests/modsys/functors/T015.icry b/tests/modsys/functors/T015.icry new file mode 100644 index 00000000..5a52d4aa --- /dev/null +++ b/tests/modsys/functors/T015.icry @@ -0,0 +1 @@ +:load T015.cry diff --git a/tests/modsys/functors/T015.icry.stdout b/tests/modsys/functors/T015.icry.stdout new file mode 100644 index 00000000..953adc64 --- /dev/null +++ b/tests/modsys/functors/T015.icry.stdout @@ -0,0 +1,4 @@ +Loading module Cryptol +Loading module Cryptol +Loading interface module T015_S +Loading module Main diff --git a/tests/modsys/functors/T015_S.cry b/tests/modsys/functors/T015_S.cry new file mode 100644 index 00000000..5b7a19d2 --- /dev/null +++ b/tests/modsys/functors/T015_S.cry @@ -0,0 +1,7 @@ +interface module T015_S where + +type n : * + +type constraint (Literal 0 n) + +