CODEWITHSUNDEEP
coq
Charlie Parker
Charlie Parker

Reputation: 5209

What does the at sign @ mean in Coq - especially in the context of Gallina terms?

I was trying to understand what the @ at sign did in Coq in all contexts. The context that I saw this was that I was experimenting with printing and removing notations (or as much as I could) in Coq. In particular, I was printing (Gallina) terms with the Set Printing All. I defined my own addition and nats and got this when I did that

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)

but I wasn't sure what the @ sign meant. What does it mean?

Note I saw this question Refine and @ (at) symbol in Coq 8.5pl1 but it seems that they are using @ in the context of a proof where I am seeing it in a different context (I am printing a Gallina term). To be honest I don't fully appreciate the answer to that question. Perhaps it is related to my question but I cannot tell. Perhaps from reading that more carefully I might need implicit arguments to really appreciate what @ mean? To my surprise googling What does the at sign @ in coq do didn't yield to much except that SO question I posted. A reference to the coq manual/documentation wouod be ideal (I did try to search in the docs at sign and @ but it didn't yield anything useful).

Perhaps I can share my script:

    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.

Upvotes: 3

Views: 423

Answers (1)

Li-yao Xia
Li-yao Xia

Reputation: 33519

@ disables implicit arguments (cf Reference Manual). The first argument of eq_refl is implicit, so @eq_refl A b is eq_refl b with an implicit A.

Upvotes: 7

Related Questions