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]))
_______________________________________________
Ur mailing list
[email protected]
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
