coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Formalisation of the Hilbert's choice operator

From: feliot AT noos.fr
To: coq-club AT pauillac.inria.fr
Subject: Formalisation of the Hilbert's choice operator
Date: Wed, 25 Jul 2001 21:15:33 +0200

I working on lattices and ordered structure in coq.

How can be formalize thz Hilbert's choice operator in coq

Thanks for your help

--
Claude FELIOT
feliot AT noos.fr

Formalisation of the Hilbert's choice operator, feliot