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. Hans
