The Coq mailing list

[Kirill Taran <kirill.t256 AT gmail.com>]

Guillaume Melquiond,

Really, it's very easy and clear; thanks.

Sincerely,
Kirill Taran

On Sat, Feb 8, 2014 at 3:19 PM, Guillaume Melquiond <guillaume.melquiond AT inria.fr> wrote:

On 08/02/2014 12:05, Kirill Taran wrote:

Is it true that if we had possibility to write non-terminating programs
(suppose we don't use non-terminating term in types, so type check
terminates) then we would have possibility to prove everything?

Fixpoint f (x : unit) : False := f x.
Goal False. exact (f tt). Qed.

Best regards,

Guillaume