From 5f0844f69cb9eb5d06c321edf66e921f63dacf3f Mon Sep 17 00:00:00 2001 From: aarne Date: Mon, 12 Apr 2010 21:06:11 +0000 Subject: [PATCH] restored table3 in Coordination; completed PhrasebookFre --- src/prelude/Coordination.gf | 18 ++++++++++++++---- 1 file changed, 14 insertions(+), 4 deletions(-) diff --git a/src/prelude/Coordination.gf b/src/prelude/Coordination.gf index b9fc7a25e..13081d255 100644 --- a/src/prelude/Coordination.gf +++ b/src/prelude/Coordination.gf @@ -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 } ;