John Lång

Exercise Suggestion: Pi-syntax

7

Hi. I like this book a lot, but I think it could have more exercises. In the quantifiers chapter, there's an example on the use of the `syntax` keyword that...

Instructions for running LiquidHaskell

2

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...

Chapter 12 Exercise InsertRight

4

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...

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...

Links to subsections don't work for me

2

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...

Chapter 8 exercise "reverse"

8

For reference, here's the template given in the material: ``` {-@ assume reverse :: xs:UList a -> UList a @-} reverse :: [a] -> [a] reverse = go [] where...

Syntax of refinement types

4

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...