Thank you, this works with Z3:
// safe subtract pred
stacst safesub_b : (int, int) -> bool
extern praxi lemma_safesub_b { m,n:nat | n <= m }
() : [safesub_b (m,n)] unit_p
fun mysub_b { m,n:nat | n <= m }
(x:int m, y:int n) : [safesub_b (m,n)] int
= let prval () = $solver_assert (lemma_safesu
stream_vt is pretty similar to the linear hom you used.
Essentially, stream_vt is a linear hom whose arity equals 0.
On Wednesday, April 19, 2017 at 10:10:29 AM UTC-4, August Alm wrote:
>
> Thank you! Still learning how to handle laziness. =)
>
> Den onsdag 19 april 2017 kl. 15:56:42 UTC+2 skrev g
Thank you! Still learning how to handle laziness. =)
Den onsdag 19 april 2017 kl. 15:56:42 UTC+2 skrev gmhwxi:
>
> The 'free' part of from_vt should be dropped:
>
> val
> from_vt =
> fix f(i: int): stream_vt(int) =>
> $ldelay(stream_vt_cons{int}(i, f(i+1)))
>
> stream_vt_head_exn tries to free a g
Wow, thank you Kiwamu, you just made my document looks way more colorful :)
On Tuesday, April 18, 2017 at 2:04:40 AM UTC-4, Artyom Shalkhakov wrote:
>
> On Tuesday, April 18, 2017 at 10:34:48 AM UTC+6, Kiwamu Okabe wrote:
>>
>> Yes :)
>>
>
> Implement silently, don't tell anyone. Have it spring up
The 'free' part of from_vt should be dropped:
val
from_vt =
fix f(i: int): stream_vt(int) =>
$ldelay(stream_vt_cons{int}(i, f(i+1)))
stream_vt_head_exn tries to free a given stream. In the above case,
freeing the given stream trigger infinite computation.
In the follow code, 'ns' is leaked:
val
Hi!
The following code compiles but segfaults when run:
val from_vt_nine = from_vt(9)
val nine = stream_vt_head_exn(from_vt_nine)
val () = println!(nine: int)
The follwing code, on the other hand, executes as expected:
val from_vt_nine = from_vt(9)
v
