diff --git a/test/interpdef1.ivy b/test/interpdef1.ivy new file mode 100644 index 00000000..d988ceaf --- /dev/null +++ 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