summaryrefslogtreecommitdiff
path: root/transfer/examples/disjpatt.tra
diff options
context:
space:
mode:
authorbringert <bringert@cs.chalmers.se>2005-12-06 16:33:40 +0000
committerbringert <bringert@cs.chalmers.se>2005-12-06 16:33:40 +0000
commitc703a92136ce579282c63c6e31fff76cc84b37ce (patch)
treee0dedf8972756fa1322bb4d8a0c621a629bedc1e /transfer/examples/disjpatt.tra
parentee4adf5ba8ff50b4580a18d197f9e05d36195ede (diff)
Transfer: Changed transfer program file extension from .tr to .tra to avoid collision with Troff file extension.
Diffstat (limited to 'transfer/examples/disjpatt.tra')
-rw-r--r--transfer/examples/disjpatt.tra24
1 files changed, 24 insertions, 0 deletions
diff --git a/transfer/examples/disjpatt.tra b/transfer/examples/disjpatt.tra
new file mode 100644
index 000000000..740e08a7b
--- /dev/null
+++ b/transfer/examples/disjpatt.tra
@@ -0,0 +1,24 @@
+data Cat : Type where
+ VarOrWild : Cat
+ Exp : Cat
+ Ident : Cat
+
+data Tree : Cat -> Type where
+ EAbs : Tree VarOrWild -> Tree Exp -> Tree Exp
+ EPi : Tree VarOrWild -> Tree Exp -> Tree Exp -> Tree Exp
+ EVar : Tree Ident -> Tree Exp
+ EType : Tree Exp
+ EStr : String -> Tree Exp
+ EInt : Integer -> Tree Exp
+ VVar : Tree Ident -> Tree VarOrWild
+ VWild : Tree VarOrWild
+ Ident : String -> Tree Ident
+
+
+f e = case e of
+ EAbs (VWild || VVar _) e || EPi (VWild || VVar _) _ e -> doSomething e
+ Ident i -> Ident i
+ _ -> catchAll
+
+
+g (Ident x || EAbs (VWild || VVar _) t e) = x e \ No newline at end of file