[Ur] function and signature

[Adam Chlipala]

Gergely Buday wrote:
> My trial is
> val computeRecordz: r ::: {Type} ->  [ r ~ [Here] ] ->  [ r ~ [There] ] ->   ...
>                            ->  Basis.list {1 : Basis.bool, 2 :
> Basis.list $( r ++ [Here = myType, There = myType]) }
>
> but it invokes some syntax error messages. What is wrong with this?
>    

Disjointness constraints have "=>" after them, not "->".

And it will be nicer to replace

Basis.list {1 : Basis.bool, 2 : Basis.list $( r ++ [Here = myType, There 
= myType]) }

with

list (bool * list $(r ++ [Here = myType, There = myType]))