Coq隐式参数与部分应用结合：调整隐式参数插入顺序方法咨询

针对你的需求有三种常用实现方式，都可以达到延迟隐式参数插入的效果：

• 手动封装调整参数顺序（适合长期高频使用）
  你可以手动定义一个新的包装函数，翻转参数的排列顺序，将nat参数放到隐式参数A之前：

Definition foo_delayed (n : nat) {A : Type} (x : A) := @foo A n x.

定义后foo_delayed的类型正好是你需要的nat -> forall A : Type, A -> A，后续可以直接做部分应用：

(* 直接给第一个参数传1，得到的foo_1类型为forall A : Type, A -> A *)
Definition foo_1 := foo_delayed 1.

• 临时使用无需额外定义
  如果只是偶尔需要这种部分应用，不需要额外定义新函数，可以直接用@显式展开所有隐式参数，将隐式参数位留空让Coq后续自动推导：

(* @foo会把所有隐式参数转为显式，第一个参数A留空，直接传入第二个参数1 *)
Definition foo_1 := @foo _ 1.

这种写法得到的foo_1类型和上面包装后的结果完全一致，效果等同于你提到的@(foo 1)语法。

• 自定义语法糖（最贴近你提到的@(foo 1)写法）
  你可以通过Coq的记号系统自定义快捷语法，后续可以直接用类似你描述的写法调用：

(* 定义自定义记号，@@f x 等价于 @f _ x *)
Notation "'@@' f x" := (@f _ x) (at level 10, f at next level).

(* 直接用自定义语法调用 *)
Definition foo_1 := @@foo 1.

内容的提问来源于stack exchange，提问作者pjm