at 符号 @ 在 Coq 中意味着什么 - 特别是在 Gallina 术语的上下文中？

Question

我试图理解@at 符号在 Coq 中在所有情况下的作用。我看到这个的背景是我正在 Coq 中尝试打印和删除符号（或尽可能多）。特别是，我用 . 打印 (Gallina) 术语Set Printing All。我定义了自己的加法和 nat，当我这样做时得到了这个

my_add_eq = 
fun x y : my_nat => @eq_refl my_nat (my_add x y)
     : forall x y : my_nat, @eq my_nat (my_add x y) (my_add x y)

但我不确定这个@标志是什么意思。这是什么意思？

---

请注意，我在 Coq 8.5pl1 中看到了这个问题 Refine 和 @ (at) 符号，但它们似乎@在证明的上下文中使用，而我在不同的上下文中看到它（我正在打印 Gallina 术语）。老实说，我并不完全理解这个问题的答案。也许这与我的问题有关，但我不能说。也许通过更仔细地阅读，我可能需要隐含的论据才能真正理解什么@意思？令我惊讶的是，What does the at sign @ in coq do除了我发布的那个问题之外，谷歌搜索并没有得到太多结果。对 coq 手册/文档的参考将是理想的选择（我确实尝试在文档中搜索at sign，@但没有产生任何有用的结果）。

---

也许我可以分享我的脚本：

    Inductive my_nat : Type :=
    | O : my_nat
    | S : my_nat->my_nat.

    Fixpoint my_add (n1:my_nat) (n2:my_nat) :=
        match n1 with
            | O => n2
            | S n1' => S (my_add (n1') (n2))
        end.

    Notation "x [+] y" := (my_add x y)
                       (at level 50, left associativity)
                       : nat_scope.

    Lemma my_add_eq:
      forall (x y : my_nat),
        x [+] y = x [+] y.
    Proof.
      auto.
    Qed.
    
    Print my_add_eq.
    Set Printing All.
    Print my_add_eq.

Answer 1

@禁用隐式参数（参见参考手册）。的第一个参数eq_refl是隐式的，因此@eq_refl A b隐eq_refl b式A。