summaryrefslogtreecommitdiff
path: root/test-suite/output/Cases.out
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/output/Cases.out')
-rw-r--r--test-suite/output/Cases.out4
1 files changed, 4 insertions, 0 deletions
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
new file mode 100644
index 00000000..5f13caaf
--- /dev/null
+++ b/test-suite/output/Cases.out
@@ -0,0 +1,4 @@
+t_rect =
+[P:(t->Type); f:([x:=t](x0:x)(P x0)->(P (k x0)))]
+ Fix F{F [t:t] : (P t) := <P>Cases t of (k x x0) => (f x0 (F x0)) end}
+ : (P:(t->Type))([x:=t](x0:x)(P x0)->(P (k x0)))->(t:t)(P t)