Adding various tests for mutual records.

1 files changed, 57 insertions, 0 deletions

diff --git a/test-suite/success/mutual_record.v b/test-suite/success/mutual_record.v
new file mode 100644
index 000000000..77529733b
--- /dev/null
+++ b/test-suite/success/mutual_record.v
@@ -0,0 +1,57 @@
+Module M0.
+
+Inductive foo (A : Type) := Foo {
+  foo0 : option (bar A);
+  foo1 : nat;
+  foo2 := foo1 = 0;
+  foo3 : foo2;
+}
+
+with bar (A : Type) := Bar {
+  bar0 : A;
+  bar1 := 0;
+  bar2 : bar1 = 0;
+  bar3 : nat -> foo A;
+}.
+
+End M0.
+
+Module M1.
+
+Set Primitive Projections.
+
+Inductive foo (A : Type) := Foo {
+  foo0 : option (bar A);
+  foo1 : nat;
+  foo2 := foo1 = 0;
+  foo3 : foo2;
+}
+
+with bar (A : Type) := Bar {
+  bar0 : A;
+  bar1 := 0;
+  bar2 : bar1 = 0;
+  bar3 : nat -> foo A;
+}.
+
+End M1.
+
+Module M2.
+
+Set Primitive Projections.
+
+CoInductive foo (A : Type) := Foo {
+  foo0 : option (bar A);
+  foo1 : nat;
+  foo2 := foo1 = 0;
+  foo3 : foo2;
+}
+
+with bar (A : Type) := Bar {
+  bar0 : A;
+  bar1 := 0;
+  bar2 : bar1 = 0;
+  bar3 : nat -> foo A;
+}.
+
+End M2.