On Tue, 30 Sep 2008 03:27:09 -0600 "Luke Palmer" <[EMAIL PROTECTED]> 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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
