Is it possible to use symbols like $\mathbb{N},\forall,\implies$ in Coq?
Add a comment
|
2 Answers
$\begingroup$
$\endgroup$
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.
Examples:
Notation "ℕ" := nat.
Notation "'⟦' x ; x0 '⟧'" := (x, x0) (at level 10, x at next level, x0 at next level).
$\begingroup$
$\endgroup$
4
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.
answered Apr 3 at 12:54
-
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$ Commented Apr 3 at 14:10
-
-
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$ Commented Apr 3 at 19:48
-