forked from GitHub/gf-core
relatives (but expensive)
This commit is contained in:
@@ -11,11 +11,7 @@ abstract Predic = Categories ** {
|
||||
Vt : CType -> VType ;
|
||||
VtN : CType -> VType ;
|
||||
|
||||
CtN,
|
||||
CtS,
|
||||
CtV,
|
||||
CtQ,
|
||||
CtA : CType ;
|
||||
CtN, CtS, CtV, CtQ, CtA : CType ;
|
||||
|
||||
SPredVerb : (v : VType) -> NP -> Verb v -> Compl v -> Cl ;
|
||||
|
||||
@@ -23,22 +19,14 @@ abstract Predic = Categories ** {
|
||||
RPredVerb : (v : VType) -> RP -> Verb v -> Compl v -> RCl ;
|
||||
IPredVerb : (v : VType) -> Verb v -> Compl v -> VCl ;
|
||||
|
||||
ComplNil : Compl Vt_ ;
|
||||
ComplNP : NP -> Compl (Vt CtN) ;
|
||||
ComplS : S -> Compl (Vt CtS) ;
|
||||
ComplQ : QS -> Compl (Vt CtQ) ;
|
||||
ComplA : AP -> Compl (Vt CtQ) ;
|
||||
Compl_ : Compl Vt_ ;
|
||||
ComplN : NP -> Compl (Vt CtN) ;
|
||||
ComplS : S -> Compl (Vt CtS) ;
|
||||
ComplQ : QS -> Compl (Vt CtQ) ;
|
||||
ComplA : AP -> Compl (Vt CtQ) ;
|
||||
|
||||
ComplAdd : (c : CType) -> NP -> Compl (Vt c) -> Compl (VtN c) ;
|
||||
|
||||
{-
|
||||
MkSlash3 : NG NtS -> VG (VtN CtN) -> CG (Vt CtN) -> Slash ;
|
||||
MkSlash2 : (c : CType) -> NG NtS -> VG (VtN c) -> CG (Vt c) -> Slash ;
|
||||
MkSlash1 : NG NtS -> VG (Vt CtN) -> Slash ;
|
||||
SlashQ : NG NtQ -> Slash -> SG NtQ ;
|
||||
-}
|
||||
|
||||
|
||||
VeV1 : V -> Verb Vt_ ;
|
||||
VeV2 : V2 -> Verb (Vt CtN) ;
|
||||
VeVS : VS -> Verb (Vt CtS) ;
|
||||
@@ -47,3 +35,10 @@ abstract Predic = Categories ** {
|
||||
VeV2Q : V2Q -> Verb (VtN CtQ) ;
|
||||
---- etc
|
||||
}
|
||||
|
||||
{-
|
||||
MkSlash3 : NG NtS -> VG (VtN CtN) -> CG (Vt CtN) -> Slash ;
|
||||
MkSlash2 : (c : CType) -> NG NtS -> VG (VtN c) -> CG (Vt c) -> Slash ;
|
||||
MkSlash1 : NG NtS -> VG (Vt CtN) -> Slash ;
|
||||
SlashQ : NG NtQ -> Slash -> SG NtQ ;
|
||||
-}
|
||||
|
||||
Reference in New Issue
Block a user