coq - 函数参数可以在 Coq 中自动限定范围吗？

Question

假设我正在一个经常混合 nat 和 Z 的环境中工作。例如，如果我有

Require Import List ZArith.
Import ListNotations.
Open Scope Z_scope.
Definition f (l : list nat) := l.
Compute f [1;3].

Coq 告诉我我The term "[1; 3]" has type "list Z" while it is expected to have type "list nat". 当然可以写[1;3]%nat，但我想知道是否有更好的方法，因为通常没有歧义。

一个相关的问题是：我可以避免手动定义符号参数的范围吗？

Notation "\\\ l ///" := (f l).
Compute \\\[1;3]///. (* same error as before *)

标签： coq