The Coq mailing list

[Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>]

Hi,

Thanks for your explanations about decidability. Very interesting,
made me think a lot, I think a true definition of decidability in
Coq should be very complicated, since it implies that we define the
notion of algorithm, and tutti quanti. I think Bruno Barras' thesis
(Coq in Coq) contains this.

-- 
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/