Termination checking in the tutorial

[Michael Misamore]

Hi guys,

Going through the tutorial now and getting excited about LiquidHaskell! I'm working through it in Vim and noticed that some of the examples require additional annotations. The latest example was

http://ucsd-progsys.github.io/liquidhaskell-tutorial/05-datatypes.html#/orderedlists

in which I needed to add an {-@ autosize IncList @-} annotation to satisfy the termination checker for the "insert" function in insertion sort. I actually prefer doing this to just disabling the checker. Should I submit PRs as I find these newbie issues or just raise them here?

Thanks,
Michael

[Ranjit Jhala]

Hi Michael,

Yes -- since the tutorial was written, we made

termination & totality "opt-out" (on by default)

rather than "opt-in" (off by default).

[In fact, the tutorial _desperately_ needs a chapter

on termination checking, need to work on it ASAP!]

If you can submit PRs those would be best, but if not,

issues would be great too.

Many thanks!

- Ranjit.

--
You received this message because you are subscribed to the Google Groups "liquidhaskell" group.
To unsubscribe from this group and stop receiving emails from it, send an email to liquidhaskell+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.