Thanks! That solves that.
Arets Paeglis
about.me/mindbound
On Wed, Oct 19, 2016 at 6:22 AM, gmhwxi wrote:
> RT(Any) is a type (not a value).
>
> You need something like:
>
> extern
> fun RT_of_int : {n:int} int(n) -> RT(n)
>
> val m = @{ rt = RT_of_int(0) } : M
>
> On Tuesday, October 18, 2016
RT(Any) is a type (not a value).
You need something like:
extern
fun RT_of_int : {n:int} int(n) -> RT(n)
val m = @{ rt = RT_of_int(0) } : M
On Tuesday, October 18, 2016 at 11:03:31 PM UTC-4, Arets Paeglis wrote:
>
> You're correct, although that didn't solve the issue itself (type
> checking s
You're correct, although that didn't solve the issue itself (type
checking still fails with the same error).
Arets Paeglis
about.me/mindbound
On Wed, Oct 19, 2016 at 5:47 AM, gmhwxi wrote:
>
> {a:int} means universal quantification.
> What you need is probably existential quantification:
>
>
>
{a:int} means universal quantification.
What you need is probably existential quantification:
typedef M = @{
rt = [a:int] RT(a)
}
On Tuesday, October 18, 2016 at 10:44:11 PM UTC-4, Arets Paeglis wrote:
>
> Hi,
>
> Assuming we have a record and its supporting definitions as follows,
> abst@
Hi,
Assuming we have a record and its supporting definitions as follows,
abst@ype RT(int) = int
stadef Any = 0
typedef M = @{
rt = {a: int} RT(a)
}
what is the proper way of initialising a value of type M? Doing
val m = @{ rt = RT(Any) } : M
fails with error(2): the dynamic identifier [Re
