associativity of implication

[DanGrayson]

The associativity of implication, A ⇒ B, is wrong, since it differs from that of A -> B.

Reserved Notation "A ⇒ B" (at level 95, no associativity).
(* to input: type "\Rightarrow" or "\r=" or "\r" or "\Longrightarrow" or "\=>" with
             Agda input method *)

Notation "A ⇒ B" := (himpl A B) : logic.

[arnoudvanderleer]

@DanGrayson Is this still relevant?

[benediktahrens]

I think it would be fine to change the associativity to align with that of function types.