test for definition-in

jsiek · Jan 7, 2025 · 4ddebe2 · 4ddebe2
1 parent c28aec5
commit 4ddebe2
Showing 1 changed file with 11 additions and 0 deletions.
diff --git a/test/should-pass/definition_in.pf b/test/should-pass/definition_in.pf
@@ -0,0 +1,11 @@
+import Nat
+
+define x = 0
+define y = 1
+
+theorem T: all z:Nat. if z = x + y then z = 1
+proof
+  arbitrary z:Nat
+  assume zxy: z = x + y
+  definition {x,y,operator+} in zxy
+end