ucsd-progsys/liquidhaskell — pull request #180 by gridaphobe (2014-02-28 23:19:00+00:00)
Title: Repeat returns a list of Cons's

We can prove that `repeat` returns a `List` with no `Nil`s, and that we can safely `take` any number of elements from `repeat`.

The code is somewhat hacky, I've changed `refresh` to only expand `Ref`s twice so we don't get an infinite loop when trying to expand a recursive `Ref`. This required changing a few `safeZip`s in `Constraint` to regular `zip`s because not all instances of an `RApp` will have the correct number of `Ref`s.. But it works empirically, i.e. none of our existing tests break..