liquidhaskell-tutorial
liquidhaskell-tutorial copied to clipboard
ucsd-progsys
Tutorial for LiquidHaskell
The first chapter of the tutorial only tells how to run the chapters of the book using `stack`. I think that instructions for installing LiquidHaskell and running it from a...
The "safe head" exercise asks us to write a specification for `null`: ``` Write down a specification for `null` such that `safeHead` is verified. Do *not* force `null` to only...
**OS**: WSL2 (Ubuntu) on Windows 10 **Commit I cloned this repository at**: 8bf919a9d81f34ea7675dbe112086151d14d57c7 **z3 version**: 4.8.7-4build1 Hi LiquidHaskell team, I wanted to start the tutorial so I cloned this repository...
I get errors when I try to define `insR`symmetrically to how `insL`has been defined above. However, these errors are about `insL` rather than `insR`. How can it be? These are...
The link in the readme 404s, and I could not find a similarly-named repo under `ucsd-progsys`. As it is, working through the tutorial is rather difficult without them.
Maybe I've understood the definitions wrong but it seems to me that Figures 1.4 and 1.5 in Chapter 12 are incorrect. Shouldn't the node labelled `v` be on level `n...
When I browse the HTML version of the book at [https://ucsd-progsys.github.io/liquidhaskell-tutorial](https://ucsd-progsys.github.io/liquidhaskell-tutorial) and click the heading of a subsection from the table of contents, Firefox takes me to the beginning of...
For reference, here's the template given in the material: ``` {-@ assume reverse :: xs:UList a -> UList a @-} reverse :: [a] -> [a] reverse = go [] where...
I've read through the chapters 1 to 7 and haven't come accross a definition of the syntax of refinement types. I was expecting to see it rather early in the...
The function `delmin` in Chapter 5.3 seems to have a problem. I get the following error: ``` ~/liquidhaskell-tutorial/src/Tutorial_05_Datatypes.lhs:663:30: error: Liquid Type Mismatch . The inferred type VV : {v :...