ucsd-progsys/liquidhaskell — pull request #205 by nikivazou (2014-05-04 19:06:49+00:00)
Title: Invariants

Enable checkable invariants (ie., at each call of a data-constructor LH proves that the invariant holds) via "using" annotation:

~~~
{-@ using (F a) as {v : F a | (fy v) = (fx v) } @-}
~~~

See:
[tests/pos/Invariants.hs](https://github.com/ucsd-progsys/liquidhaskell/blob/invariants/tests/pos/Invariants.hs) and [tests/neg/Invariants.hs](https://github.com/ucsd-progsys/liquidhaskell/blob/invariants/tests/neg/Invariants.hs)