liquidhaskell

Hello everyone, I have just defended my master's thesis about liquid types for verification of

Hi Thomas, (sorry for the delay - I think the slack channel may receive quicker replies!) Thanks for

Hi Kishlaya I replied to this on SO -- LMK if the answer doesn't make sense! https://

I was trying to add/fix the type signature for the function `primes` (as defined on the homepage of

I want to write a smarted Foreign.Storable that enforces a lower bound on pointer length based on the

Hello Ranjit, Thanks for the reply! I will see if I can minimize the examples more and post the

Hi Marcio, I would suggest using “stack” to get avoid this problem. If you do stack install vector

The workaround works with my code. Thanks very much for the prompt response! I thought I was going

That fixed it. Thanks very much! On Monday, 22 January 2018 13:27:22 UTC-5, Ranjit Jhala wrote: Hi

Hello, Ran into another little snag in the tutorial: trying to lift "fst" and "snd

That fixed it. Thanks so much Ranjit! I didn't get to the chapter on Refinement Reflection yet

Hi Michael, Yes -- since the tutorial was written, we made termination & totality "opt-out

Hmm, great question! Ithink the short answer is “I don't know” As this has long been an item on

Oooh ok ! Thank you! :) (Yep, I was typing them myself haha) El lun., 20 mar. 2017 a las 13:04,

Yes, I can run liquid from the command prompt. I tried putting it in /usr/local/bin and $HOME/.local/

Well, you are not doing anything wrong, it has to do with type class constrains. Here is a version

Thank you Niki. In the Haskell version, we use `t` and `v` (both of kind (promoted) `Nat`) as in `

Ok, Ranjit, thank you for help!

1. When I define `VecN t N`, the value parameter has to come after the type parameter (otherwise I

Yes -- the abstract refinements stuff *is* implemented in LH.. On Tue, Nov 15, 2016 at 10:34 PM,

Thanks for that. Everything appears to be working fine now. On Tuesday, June 21, 2016 at 5:47:39 AM

That did the trick. Thanks a lot. On Tuesday, June 21, 2016 at 2:13:53 AM UTC+10, Niki Vazou wrote: `

Not exactly sure what is going on with the spec files, I suspect there is a bug, but will look into

Yes, my pingVia works, LH does not complain about it. I tried the way you suggested too, without

​Hi Mi​chael -- (Apologies for the delay with the mailing list!) Thanks for pointing this out! This

We do have a limited support for per instance refinements! Here is how you can write your example

Definitely the term-level version will be easier to encode. Using bounds, we use the curly braces {x:

That is correct. Indeed, this would be an interesting feature to have! On Tue, Feb 23, 2016 at 12:53

Yes! It makes a lot of sense. I've been staying away from abstract refinements for now, but they

Is it possible to have Cabal call Liquid Haskell on a selection of modules from my Haskell projects?