coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] binary distribution for Leopard (and Snow Leopard), Thorsten Altenkirch
- Re: [Coq-Club] binary distribution for Leopard (and Snow Leopard),
Matthieu Sozeau
- [Coq-Club] what are "levels" in Coq,
Vladimir Voevodsky
- Re: [Coq-Club] what are "levels" in Coq, Adam Chlipala
- Re: [Coq-Club] what are "levels" in Coq,
harke
- Re: [Coq-Club] what are "levels" in Coq,
Vladimir Voevodsky
- Re: [Coq-Club] what are "levels" in Coq, Adam Chlipala
- Re: [Coq-Club] what are "levels" in Coq,
Thorsten Altenkirch
- Re: [Coq-Club] what are "levels" in Coq,
Yves Bertot
- Re: [Coq-Club] what are "levels" in Coq, Lionel Elie Mamane
- [Coq-Club] Type hierarchy,
Jean-Francois Dufourd
- Re: [Coq-Club] Type hierarchy, André Hirschowitz
- Re: [Coq-Club] Type hierarchy, Hugo Herbelin
- Re: [Coq-Club] Type hierarchy, Adam Chlipala
- Re: [Coq-Club] Type hierarchy, Hugo Herbelin
- Re: [Coq-Club] Type hierarchy, Jean-Francois Dufourd
- Re: [Coq-Club] what are "levels" in Coq,
Yves Bertot
- [Coq-Club] an inductive types question, Vladimir Voevodsky
- Re: [Coq-Club] an inductive types question, Adam Chlipala
- Re: [Coq-Club] an inductive types question, Vladimir Voevodsky
- Re: [Coq-Club] an inductive types question, Vladimir Voevodsky
- Re: [Coq-Club] what are "levels" in Coq,
Vladimir Voevodsky
- [Coq-Club] what are "levels" in Coq,
Vladimir Voevodsky
- Re: [Coq-Club] binary distribution for Leopard (and Snow Leopard),
Matthieu Sozeau
Archive powered by MhonArc 2.6.16.