[ re #610 ] just to make sure we don't have irrelevant constructors

agda · Feb 11, 2016 · edbc590 · edbc590
1 parent 5e30170
commit edbc590
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 0 deletions.
diff --git a/test/Fail/IrrelevantConstructor.agda b/test/Fail/IrrelevantConstructor.agda
@@ -0,0 +1,6 @@
+-- Andreas, 2016-02-11. Irrelevant constructors are not (yet?) supported
+
+data D : Set where
+  .c : D
+
+-- Should fail, e.g., with parse error.
diff --git a/test/Fail/IrrelevantConstructor.err b/test/Fail/IrrelevantConstructor.err
@@ -0,0 +1,6 @@
+IrrelevantConstructor.agda:4,3-3
+IrrelevantConstructor.agda:4,3: Parse error
+.<ERROR>
+c : D
+
+-- Should fail, e.g., w...