Is it possible to use symbols like $\mathbb{N},\forall,\implies$ in Coq?


2 Answers 2


Coq ships with basic UTF8 symbols for logic, and some other kinds of stuff that you may find helpful:

$\wedge, \vee, \rightarrow, \leftrightarrow, \forall, \exists, \neg, \neq, \le, \ge, \lambda x.e$.

Require Import Unicode.Utf8.

is all you need.

Be aware, however, that Coq's stdlib support for unicode symbols is quite limited (not like Agda). For other symbols like what you have suggested ($\mathbb{N}, \implies$), unfortunately, Coq does not provide such things, but you can certainly do it yourself by leveraging the Notation system.


Notation "ℕ" := nat.
Notation "'⟦' x ; x0 '⟧'" := (x, x0) (at level 10, x at next level, x0 at next level).

Yes. Some of these notations are already given in the Utf8_core and Utf8 modules, that you can simply import. For the others, you can add them yourselves in a similar fashion.

  • 3
    $\begingroup$ Perhaps it's worth showing a simple working example, so beginners don't have to spend an hour figuring out the correct import statement? $\endgroup$ Apr 3 at 14:10
  • $\begingroup$ it would be great $\endgroup$ Apr 3 at 15:56
  • 1
    $\begingroup$ Looking at : github.com/coq/coq/blob/… and github.com/coq/coq/blob/… should be quite self contained. To use this files: ` Require Import Utf8 Utf8_core. ` $\endgroup$ Apr 3 at 19:48
  • $\begingroup$ I rest my case :-) $\endgroup$ Apr 5 at 7:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.