Added aggregation example.

This commit is contained in:
bringert
2005-12-05 16:45:11 +00:00
parent ccb780361f
commit 224d2451d7
6 changed files with 150 additions and 0 deletions

View File

@@ -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
}