yanhasu

I suggest: * Finding the source code for [the most up to date tutorial](https://goto.ucsd.edu/~nvazou/cufp15_liquidHaskell/) (maybe @nikivazou knows where it is?) and putting it somewhere prominent (e.g. this repo, its own...

Here's an even more complete version: https://github.com/ucsd-progsys/intro-refinement-types

Sounds good, PR incoming!

On [the current demo](http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1637596937_657.hs), `lazy` seems to postulate finite return type ('`Fin` type') as well eventual reduction to WHNF ('`Wnf` type'). So I'm guessing that `Wnf` has been jettisoned as...

I see three issues: 1. **Linking** is poor, so newbies miss out on half the information 2. **Styles** are different, suggesting that one of the sites is abandoned or unofficial...

Whilst we're changing the syntax, why not de-tuple the abstract refinements? e.g. writing `type BST a = BinaryTree a LessThan root> GreaterThan root>` seems slightly more Haskell-y than `type BST...

@nikivazou I haven't written anything yet, but I'm willing to have a go at implementing this.

@ranjitjhala some other points about the new proposal: * The curly braces `{` `}` are already highly overloaded (HS records, HS layout, LH refinements, LH refinements of `()`, ...). *...

Hello, could I have access too please?

Yes, thanks!