Search code examples
coq

What does "eq^~" mean in Coq?

When I write 'Print Qeq_trans.' in the CoqIde, I can see many 'eq^~' expressions in message window.

For example, eq^~ (Qnum z * QDen x * QDen y)%Z.

Please let me know the meaning of this term.

Solution

  • I think it is a way to apply a function to only its second argument. Do a

    Locate "_ ^~ _".

    to get the definition.