restored table3 in Coordination; completed PhrasebookFre

This commit is contained in:
aarne
2010-04-12 21:06:11 +00:00
parent 0ed2d467a5
commit 93e3635bea
4 changed files with 51 additions and 9 deletions

View File

@@ -104,8 +104,7 @@ oper
\P,Q,R,or,xs ->
{s = \\p,q,r => or.s1++ xs.s1 ! p ! q ! r ++ or.s2 ++ xs.s2 ! p ! q ! r} ;
---------
ListTable4 : Type -> Type -> Type -> Type -> Type = \P,Q,R,T ->
ListTable4 : Type -> Type -> Type -> Type -> Type = \P,Q,R,T ->
{s1,s2 : P => Q => R => T => Str} ;
twoTable4 : (P,Q,R,T : Type) -> (_,_ : {s : P => Q => R => T => Str}) ->
@@ -153,10 +152,21 @@ oper
{s1 = table P {p => table Q {q => x.s ! p ! q ++ c ++ xs.s1 ! p ! q}} ;
s2 = xs.s2
} ;
consrTable4 : (P,Q,R,T : Type) -> Str -> {s : P => Q => R => T => Str} ->
consrTable3 : (P,Q,R : Type) -> Str -> {s : P => Q => R => Str} ->
ListTable3 P Q R -> ListTable3 P Q R =
\P,Q,R,c,x,xs ->
{s1 = table P {p => table Q {q => table R {
r => x.s ! p ! q ! r ++ c ++ xs.s1 ! p ! q ! r
}}} ;
s2 = xs.s2
} ;
consrTable4 : (P,Q,R,T : Type) -> Str -> {s : P => Q => R => T => Str} ->
ListTable4 P Q R T -> ListTable4 P Q R T =
\P,Q,R,T,c,x,xs ->
{s1 = table P {p => table Q {q => table R { r => table T {t => x.s ! p ! q ! r ! t ++ c ++ xs.s1 ! p ! q ! r ! t}}}} ;
{s1 = table P {p => table Q {q => table R {
r => table T {t => x.s ! p ! q ! r ! t ++ c ++ xs.s1 ! p ! q ! r ! t}}}} ;
s2 = xs.s2
} ;