30 Sep
2008
30 Sep
'08
6:37 a.m.
On Tue, 30 Sep 2008 03:27:09 -0600
"Luke Palmer"
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