The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

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?
> >
> > V.
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)

for expressions,

and :

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

the patterns p1, ..., mostly look like symbols and function applications.

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.

There is one special treatment with numerals, but even them can be 
entered using a function notation.
For example,  when understood as an integer (i.e., in Z_scope)  3 stands 
for Zpos (xO xH)

If you use only the syntax described here, you don't need to understand 
the notion of levels...

To know what function is hidden behind a notation, you can use Locate, 
as in the following example:

Locate "_ /\ _".
The answer that the function is actually named 'and', so that A /\ B  
can also be written (and A B).

I hope this helps.

Yves