The Coq mailing list

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

Hi Cedric,

What you observe is due to scopes:

- The + notation for plus is in scope nat_scope.
- The + notation for plus_ is "lonely" (i.e. in no scope) and it is
  hence the default interpretation in the current context.
- Interpreting < as lt_ in the first example forces its arguments to
  be preferably interpreted in nat_scope (because the type of the
  arguments of lt_, nat, is bound to nat_scope), thus taking
  precedence over the interpretation of + as plus_.
- Interpreting = does not affect the scope of its arguments, hence the
  arguments of = are interpreted using the default interpretation, which
  interprets + as plus_.

More can be found in section 12.2.1 of the reference manual (Global
interpretation rules for notations).

Hugo

On Fri, Feb 25, 2011 at 10:24:01AM +0100, AUGER Cedric wrote:
> I was surprised to the result of this code after deactivating the
> display of notations:
> 
> >>>
> Definition plus_ (m n: nat) := m.
> Definition lt_ (m n: nat) := true.
> 
> Notation "n + m" := (plus_ m n).
> Notation "m < n" := (lt_ m n).
> 
> Check (forall m n, (forall o, true = (m< ( n+o ) ))).
> Check (forall n, (forall o, 0 = ( n+o ) )).
> <<<
> 
> in the first case, n+o is interpreted as the coq defined "plus", but in
> the second case it is interpreted as "plus_".
> 
> I expected "( x )" to put 'x' at level 200, so that would force the
> interpretation of "x < y" to be the same in both cases.
> 
> Is there some explanation of this thing? Has this behaviour been
> changed along coq versions?
> 
> Thanks
> Cédric.
>