[Haskell-cafe] Total Functional Programming in Haskell

[Robin Green]

On Tue, 30 Sep 2008 03:27:09 -0600
"Luke Palmer" <lrpalmer at gmail.com> wrote:

> But I *want* to do something like that with Coq  (I prefer it to Agda
> for little more than personal taste).   In particular, I'd like to see
> a reasoning framework for partial functions, so you could state and
> prove a property like:
> 
>   length [1..] = _|_

Bear in mind, in Coq, the equivalent of [1..] is a stream, whereas the
equivalent of [1,2,3] is a list. You'd have to have list functions in
Coq which worked generically over both lists and streams to be able to
say what you want, and I don't know of any existing attempt to do that.
-- 
Robin