forked from GitHub/gf-core
parameters to dep
This commit is contained in:
@@ -2,24 +2,41 @@ abstract Dep = {
|
||||
cat
|
||||
NType ;
|
||||
VType ;
|
||||
CType ;
|
||||
SG NType ;
|
||||
NG NType ;
|
||||
VG VType ;
|
||||
CG VType ;
|
||||
|
||||
Slash ;
|
||||
|
||||
fun
|
||||
NtS, NtQ : NType ;
|
||||
Vt1, Vt2, VtS : VType ;
|
||||
CtN, CtV, CtS, CtQ, CtA : CType ;
|
||||
Vt, VtN : CType -> VType ;
|
||||
Vt_ : VType ;
|
||||
|
||||
MkSG : (n : NType) -> (v : VType) -> NG n -> VG v -> CG v -> SG n ;
|
||||
|
||||
CG1 : CG Vt1 ;
|
||||
CG2 : NG NtS -> CG Vt2 ;
|
||||
CG_ : CG Vt_ ;
|
||||
CGN : NG NtS -> CG (Vt CtN) ;
|
||||
CGS : SG NtS -> CG (Vt CtS) ;
|
||||
CGQ : SG NtQ -> CG (Vt CtQ) ;
|
||||
|
||||
CGN_ : (c : CType) -> NG NtS -> CG (Vt c) -> CG (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 ;
|
||||
|
||||
John : NG NtS ;
|
||||
Who : NG NtQ ;
|
||||
|
||||
Walk : VG Vt1 ;
|
||||
Love : VG Vt2 ;
|
||||
Walk : VG Vt_ ;
|
||||
Love : VG (Vt CtN) ;
|
||||
Know : VG (Vt CtS) ;
|
||||
Give : VG (VtN CtN) ;
|
||||
Tell : VG (VtN CtS) ;
|
||||
Ask : VG (VtN CtQ) ;
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user