The Coq mailing list

[Thorsten Altenkirch <txa AT Cs.Nott.AC.UK>]

On 6 Oct 2009, at 19:19, Vladimir Voevodsky wrote:

> A related question: does Cow has an "internal representation"  
> language with a more rigid syntactic structure?
>
> V.

Coq is based on the Calculus of Inductive (and Coinductive)  
Constructions. This is a dependently typed lambda calculus with an  
impredicative universe (The Calculus of Constructions) of propositions  
extended by a predicative universe of sets which are closed under  
inductive (and coinductive) definitions. See the reference manual, the  
Coq'Art book and a number of related research papers and PhD theses.

Cheers,
Thorsten


> On Oct 6, 2009, at 2:11 PM, 
> harke AT cs.pdx.edu
>  wrote:
>
> > This is a standard trick for reducing the amount of parenthesisation
> > used by many languages that have user defined infix operators.
> >
> > You'll also notice the line:
> >
> > Reserved Notation "x /\ y" (at level 80, right associativity).
> >
> > Try the following in coqide/proofgeneral:
> >
> > Variables A B C : Prop.
> > Check A /\ (B <-> C).
> > Check (A /\ B) <-> C.
> >
> > You'll see the printout of the first shows parentheses while the  
> > second
> > omits them.  This is due to the different levels.  Then try:
> >         
> > Check (A /\ B) /\ C.
> > Check A /\ (B /\ C).
> >
> > Again, the first shows parens, the second omits, due to the right
> > associativity.
> >
> > On Tue, Oct 06, 2009 at 01:52:21PM -0400, Vladimir Voevodsky wrote:
> > > 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.
> >
> > --
> > Tom Harke
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>         http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.