> I have a function that returns
>
> Basis.list
> $(<UNIF:U16369::{Type}> ++
> [#Here = myType,
> #There = myType])
>
> according to the type checker. How can I express its signature so that it
> compiles? Is it possible to express that I have these two fixed fields and
> some others?
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?
- Gergely
_______________________________________________
Ur mailing list
[email protected]
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
