(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
(*              Rocquencourt         Orsay          Lyon                    *)
(*                                                                          *)
(*                                 Coq V6.3                                 *)
(*                               July 1st 1999                              *)
(*                                                                          *)
(****************************************************************************)
(*                                 Arith.v                                  *)
(****************************************************************************)

Require Export Le.
Require Export Lt.
Require Export Plus.
Require Export Gt.
Require Export Minus.
Require Export Mult.
Require Export Between.
Require Export Minus.

Axiom My_special_variable : nat -> nat.
Declare ML Module "g_natsyntax".

Grammar nat number :=.

Grammar command command10 :=
  natural_nat [ nat:number($c) ] -> [$c].

Grammar command atomic_pattern :=
  natural_pat [ nat:number($c) ] -> [$c].

Syntax constr
  level  0:
 myspecialvariable [<<My_special_variable>>] -> ["S"];
  level 10:
  S [<<(S $p)>>] -> [$p:"nat_printer"]
| O [<<O>>] -> [ "0" ]
.

(* $Id: Arith.v,v 1.10 1999/12/07 22:49:44 herbelin Exp $ *)



