regression test for issue #49

microsoft · Nov 4, 2019 · 0674d2b · 0674d2b
1 parent 3477e94
commit 0674d2b
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 0 deletions.
diff --git a/test/interpdef1.ivy b/test/interpdef1.ivy
@@ -0,0 +1,7 @@
+#lang ivy1.7
+type nat
+interpret nat->nat
+relation (N:nat < N:nat)
+definition (N:nat < N1) = true
+invariant X:nat<X
+invariant false
diff --git a/test/run_expects.py b/test/run_expects.py
@@ -15,6 +15,7 @@
 checks = [
     ['.',
       [
+          ['interpdef1','interpdef1.ivy: line 5: error: definition of interpreted symbol <'],
           ['whileexists1','OK'],
           ['whilesome1','OK'],
           ['whilesome2','OK'],