The Coq mailing list

[Jesper Louis Andersen <jesper.louis.andersen AT gmail.com>]

On Wed, Nov 23, 2011 at 19:56, Victor Porton

> Theorem t: True.

This is much easier to solve than you think:

Print I.

Theorem t : True.
  exact I.
Qed.

True is constructed as an inductive type with only one inhabitant, I.
Thus, if we want to prove True, we can just provide I since it is a
construction of the sole True value.

Note that in Coq, unlike mathematics, there are several ways to
express something being "True". This is, among other things, to avoid
hitting into Goedel, halting theorems, computability limitations and
so on. Others can describe this way better than I.


-- 
J.