Closed beurdouche closed 7 years ago
Thanks for pointing these out! Can you try the 49-fix-syntax-highlighting branch? It has a fix for the first one — the second one is trickier.
Does F* have any sort of extensible syntax (in the style of Coq's extensible parsing)?
@cpitclaudel Thanks Clement, I have used it yesterday and today and this branch seems to work fine, haven't encountered any glitches :) To my knowledge no F* doesn't have extensible syntax but I don't know all corners of the compiler itself.
Actually it seems that I have trouble in some cases...
I see, thanks. Can you post the text so I can copy it?
module Test
assume type t
private val blah:
b:buffer t{length b = 1} ->
Stack unit
(requires (fun h -> live h b))
(ensures (fun h0 _ h1 -> live h1 b /\ modifies_1 b h0 h1))
Thanks, that should be fixed too; I force-pushed.
Yep, looks much better ;) Thanks
Things should be better now, though the let x, y = …
is still fragile: it's tricky to tell let f x =
from let x, y =
. OTOH fun's and forall's should have better looking arguments now.
Hi Clement @cpitclaudel ! Just decided to fill some nits in the syntax highlighting that I find annoying. If you have time at some point could you have a look ? Clearly this is not an emergency... ;) Thanks a lot ! B.