Skip to Content.
Sympa Menu

coq-club - [Coq-Club] what are "levels" in Coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] what are "levels" in Coq


chronological Thread 
  • From: Vladimir Voevodsky <vladimir AT ias.edu>
  • To: Coq Club <coq-club AT pauillac.inria.fr>
  • Subject: [Coq-Club] what are "levels" in Coq
  • Date: Tue, 6 Oct 2009 13:52:21 -0400
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi,


I am trying to understand the way in which Coq treats input texts. To some extent it is explained in the first part of the reference manual, but I could not find the explanation for what "levels" are (e.g. in


Reserved Notation "x <-> y" (at level 95, no associativity).

from the Coq standard library,)

Also, is there a way to search the reference manual?

Thanks,
Vladimir.





Archive powered by MhonArc 2.6.16.

Top of Page