Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


chronological Thread 
  • From: Lionel Elie Mamane <lionel AT mamane.lu>
  • To: Coq Club <coq-club AT pauillac.inria.fr>
  • Subject: Re: [Coq-Club] what are "levels" in Coq
  • Date: Fri, 9 Oct 2009 14:55:04 +0200
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Wed, Oct 07, 2009 at 01:58:38PM +0200, Yves Bertot wrote:
> Thorsten Altenkirch wrote:
>> 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?


> I guess your question is more about using a simpler notation than
> the one with infix operators and all the special notations.  The
> answer is yes.  In principle, there is a very small language in
> which you can express all formulas of Coq.  It is basically a lambda
> calculus, so that you write:

> f a  (representing function application)

> fun (x : type) => a (representing abstraction)

> forall (x : type), type

> for types.  Of course, function applications and abstractions can
> occur in types.

> To be complete, you also need to understand the syntax of
> pattern-matching constructs:

> match e as x in e' return e'' with p1 => e1 | ... end

> For inputing data into Coq, this is basically all the syntax you
> need to know for terms.  All the rest is decoration, and is defined
> using Notation.

It would seem to me that inductives and fixpoints are another "atomic"
constructs whose syntax is part of that "minimal rigid structure".

-- 
Lionel





Archive powered by MhonArc 2.6.16.

Top of Page