Hans Aberg <haber...@telia.com> skribis: > On 13 Oct 2011, at 23:14, Ludovic Courtès wrote: > >> Did you know that Coq would only compile a function when it can prove >> that it terminates? That’s another kind of compiler-supported proof one >> quickly gets used to. > > Termination is a non-deducable property. They look at a intuitionistic subset > of programs.
Sorry, I’m not sure what you mean. What I had in mind is what they call “well-founded recursion” [0] and the idea that a recursive function must have a “decreasing argument” [1]. Thanks, Ludo’. [0] http://coq.inria.fr/refman/Reference-Manual005.html#htoc79 [1] http://coq.inria.fr/refman/Reference-Manual003.html#Fixpoint
