some new functionalities in Ger

This commit is contained in:
aarne
2017-06-05 12:46:53 +00:00
parent 7bd6b4c13a
commit df39e466bb
4 changed files with 18 additions and 6 deletions

View File

@@ -327,8 +327,11 @@ mkV2 : overload {
mkVV : V -> VV ; -- with zu
auxVV : V -> VV ; -- without zu
mkVA : V -> VA ;
mkVA : overload {
mkVA : V -> VA ;
mkVA : V -> Prep -> VA ;
} ;
mkVQ : V -> VQ ;
@@ -630,7 +633,10 @@ mkV2 : overload {
= \v,p -> prepV2 v p ** {isAux = False ; lock_V2Q = <>} ;
} ;
mkVA v = v ** {lock_VA = <>} ;
mkVA = overload {
mkVA : V -> VA = \v -> lin VA (dirV2 v) ;
mkVA : V -> Prep -> VA = \v,p -> lin VA (v ** {c2 = p}) ;
} ;
mkAS v = v ** {lock_A = <>} ;
mkA2S v p = mkA2 v p ** {lock_A = <>} ;