transfer/examples/aggregation/tree.tr


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
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 
}