The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

That is "level", not "lever". It sets a priority of the notation over others. If you try it in presence of symbols which have priority under 50 or over 60, you will not notice anything.

For associativity, try something like:

Inductive bool : Set := true | false.

Definition impl (a b : bool) := if a then true else b.

Notation "a ⇒ b" := (impl a b) (at level 50, left associativity).
Notation "a ↦ b" := (impl a b) (at level 60, right associativity).

Eval compute in (false ⇒ false ⇒ false). (* impl (impl false false) false *)
Eval compute in (false ↦ false ↦ false). (* impl false (impl false false) *)
Eval compute in (false ↦ false ⇒ false).
Eval compute in (false ⇒ false ↦ false).

2014-07-22 15:10 GMT+02:00 coqcdp <coqcdpnxj AT 163.com>:

Hi,

      Recently I have learnt a coq sentence “Notation "%":= lt (at level 50,left associativity)”，since I'm a new learner， I set the number 60 it works and when I set the number 50 it also works,

     So  I am confused,  how the number  of  lever and "left or right associatity" work there?  Does it really effect the program latter using this notation ?

    

      Yours Sincerely, D.P.Chen.

--
.../Sedrikov\...