The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

  Bonjour,

  Il faut charger Arith...

Coq < Require Arith. 

Coq < Check (4).     
(4)
     : nat

  Hugo

----------------------------------------------------------------------
  À ce propos, une possibilité à laquelle nous réfléchissons pour
mieux gérer les notations de nat, Z ou R, c'est de définir une notion
de scope, dans l'esprit de Z où les «`» définissent un scope
d'interprétation pour +, *, -, 0, 1, -3,... mais en autorisant
n'importe quel construction dans un scope, pas seulement les
applications comme pour Z.

  À chaque instant, il y aurait un scope par défaut qui pourrait
changer selon les besoins et chaque scope aurait un délimiteur de
scope pour y entrer quand il n'est pas le scope par défaut (par
exemple pour mêler nat et R) comme dans

    (INR (plus (S O) n))==(Rplus (INR (S O)) (INR n)

  qui s'écrirait

             (INR {1+n})==(INR {1})+(INR n)

  si le scope par défaut est celui de R et "{" et "}" sont les
délimiteurs du scope de l'arithmétique sur nat.

  Par ailleurs, les opérateurs pourraient aussi être définis comme
changeur de scope, comme l'exponentiation dont la notation pourrait
être définie comme

  Infix "^" Zexp : Z_scope -> nat_scope -> Z_scope.

  "Check 4" marcherait alors si le scope sur nat est le défaut.