Suppose I'm working on an environment which frequently mixes nat and Z. If for example I have
Require Import List ZArith.
Import ListNotations.
Open Scope Z_scope.
Definition f (l : list nat) := l.
Compute f [1;3].
Coq tells me The term "[1; 3]" has type "list Z" while it is expected to have type "list nat".
Of course I can just write [1;3]%nat but I was wondering if there was a better way, since usually there's no ambiguity.
A related question is: can I avoid having to scope manually a notation argument?
Notation "\\\ l ///" := (f l).
Compute \\\[1;3]///. (* same error as before *)