1
0
forked from GitHub/gf-core

coordination to built-in lists

This commit is contained in:
aarne
2005-12-02 16:56:44 +00:00
parent e9ce24ad17
commit 53a2f8383c
7 changed files with 71 additions and 46 deletions

View File

@@ -102,4 +102,17 @@ oper
comma = "," ;
-- you can also do this to right-associative lists:
consrStr : Str -> Str -> ListX -> ListX = \comma,x,xs ->
{s1 = x ++ comma ++ xs.s1 ; s2 = xs.s2 } ;
consrSS : Str -> SS -> ListX -> ListX = \comma,x,xs ->
consrStr comma x.s xs ;
consrTable : (P : Type) -> Str -> {s : P => Str} -> ListTable P -> ListTable P =
\P,c,x,xs ->
{s1 = table P {o => x.s ! o ++ c ++ xs.s1 ! o} ; s2 = xs.s2} ;
} ;