summaryrefslogtreecommitdiff
path: root/transfer/examples/aggregation/tree.tr
diff options
context:
space:
mode:
Diffstat (limited to 'transfer/examples/aggregation/tree.tr')
-rw-r--r--transfer/examples/aggregation/tree.tr20
1 files changed, 20 insertions, 0 deletions
diff --git a/transfer/examples/aggregation/tree.tr b/transfer/examples/aggregation/tree.tr
new file mode 100644
index 000000000..2e9ead648
--- /dev/null
+++ b/transfer/examples/aggregation/tree.tr
@@ -0,0 +1,20 @@
+data Cat : Type where {
+ Conj : Cat ;
+ NP : Cat ;
+ S : Cat ;
+ VP : Cat
+} ;
+data Tree : (_ : Cat)-> Type where {
+ And : Tree Conj ;
+ Bill : Tree NP ;
+ ConjNP : (_ : Tree Conj)-> (_ : Tree NP)-> (_ : Tree NP)-> Tree NP ;
+ ConjS : (_ : Tree Conj)-> (_ : Tree S)-> (_ : Tree S)-> Tree S ;
+ ConjVP : (_ : Tree Conj)-> (_ : Tree VP)-> (_ : Tree VP)-> Tree VP ;
+ John : Tree NP ;
+ Mary : Tree NP ;
+ Or : Tree Conj ;
+ Pred : (_ : Tree NP)-> (_ : Tree VP)-> Tree S ;
+ Run : Tree VP ;
+ Swim : Tree VP ;
+ Walk : Tree VP
+}