[guru-lang] r543 committed - trying out unjoin with Kevin

[guru...@googlecode.com]

Revision: 543
Author: aaron.stump
Date: Wed Oct 12 13:04:29 2011
Log: trying out unjoin with Kevin
http://code.google.com/p/guru-lang/source/detail?r=543

Modified:
/branches/1.0/tests/unjoin.g

=======================================
--- /branches/1.0/tests/unjoin.g Wed Oct 12 12:15:28 2011
+++ /branches/1.0/tests/unjoin.g Wed Oct 12 13:04:29 2011
@@ -63,7 +63,6 @@
end
end.

-%-
Define minus_lt2 : Forall
(a b:nat)(u1:{ (le b a) = tt })(u2:{ (lt Z b) = tt }).{ (lt (minus a b)
a) = tt }
:=
@@ -71,6 +70,13 @@
induction (b:nat) return
Forall(u1:{ (le b a) = tt })(u2:{ (lt Z b) = tt }).{ (lt (minus a b)
a) = tt }
with
+
+ %- Z =>
+ unjoin u2 by b_eq proving Forall(u1:{ (le b a) = tt })(u2:{ (lt Z
b) = tt }).{ (lt (minus a b) a) = tt }
+ | S b' => ...
+
+ -%
+
| default nat =>
foralli(u1:{ (le b a) = tt })(u2:{ (lt Z b) = tt }).
unjoin u2 by with
@@ -132,7 +138,7 @@
end
end
end.
--%
+

%-
| Z =>