Hi cbl,

As @kyod pointed out, we use Custom Entries in ConCert to embed the syntax of a functional language into Coq. The idea is precisely to isolate parsing rules from the usual notations of Coq.

For example, one can write something like

```
Definition x := "x".
Definition y := "y".
Definition fact := "fact".
Definition factorial_syn :=
[| fix fact (x : Nat) : Nat :=
case x : Nat return Nat of
| Zero -> 1
| Suc y -> x * (fact y)
|].
```

It will be parsed into an inductive type `expr`

representing the AST. But Custom Entries are quite experimental and there are many open issues at the Coq issue tracker. Some of them should be fixed already in Coq 8.11 (like recursive notations with the “…” pattern).

You can find simple examples here. Notations , AST and more involved examples

Also, see the official Coq documentation on Custom Entries.

I have simpler example that might help you to get started. Here I define notations for simply-typed lambda calculus. It consists of notations for types and for terms. The idea is to declare required custom entries and then define notations living in particular custom entry.

```
Declare Custom Entry ty.
Notation "'*'" := tU (in custom ty).
Notation "'ℕ'" := tNat (in custom ty at level 1).
Notation " A -> B" := (tArr A B)
(in custom ty at level 4, right associativity,
A custom ty,
B custom ty at level 4).
Declare Custom Entry lambda.
Notation "[! e !]" := e (e custom lambda at level 2).
Notation "()" := (Star) (in custom lambda).
Notation "'v0'" := (Var (here _)) (in custom lambda).
Notation " 'λ' e : τ -> σ" := (Lam τ σ e) (in custom lambda at level 1,
e custom lambda at level 2,
τ custom ty at level 2,
σ custom ty at level 2).
Notation "e1 e2" := (App _ _ e1 e2) (in custom lambda at level 1,
e1 custom lambda,
e2 custom lambda at level 2).
```

Now, everything in the brackets “[! … !]” will be parsed as a lambda term. E.g. an identity function of type `* -> *`

(meaning unit to unit)

```
Definition id_unit : Exp [] (tU :-> tU) :=
[! λ v0 : * -> * !].
```