
16 Oct
2018
16 Oct
'18
5:51 p.m.
Eric Seidel
On Tue, Oct 16, 2018, at 15:14, Ben Gamari wrote:
For this we can follow the model of Liquid Haskell: `{-@ $TOOL_NAME ... @-}`
LiquidHaskell does not use `{-@ LIQUID ... @-}`, we just write the annotation inside `{-@ ... @-}` :)
Ahh, I see. I saw [1] and assumed that all annotations included the LIQUID keyword. Apparently this isn't the case. Thanks for clarifying! Cheers, - Ben [1] https://github.com/ucsd-progsys/liquidhaskell#theorem-proving