-) in the filename?Yes it does. In fact you don’t need to do anything and you will be able to use unicode in notations.
Caution
Certain unicode characters are seen as letters, and only can be used inside identifiers. For Coq Notations however you are free to use them however you want.
You can actually even use ∀ (x : A), B instead of
forall (x : A), B, A ∧ B instead of
A /\ B, A → B instead of
A -> B and so on… as soon as you import the
Utf8 module:
From Coq Require Import Utf8.Tip
You can use the latex-input
VSCode extension (or presumably others of your liking) to enter unicode
characters easily.
Assuming you use VSCoq Legacy or CoqIDE, then the answer is mostly yes. However, you can also tell Coq to evaluate up to the point where your cursor is. In VSCoq you do it with Ctrl + Alt + → or “Interpret to point” from the commande palette (Ctrl + Shift + P).
If you use VSCoq 2 instead, then you have access to “Continuous mode” which displays the goal where your cursor is, and otherwise evaluates everything in the background. See our section on editors for more.
-) in the filename?Coq doesn’t let you use dashes in the filename (for instance if you
call it my-file.v then VSCoq will not work) because
implicitly, a filename becomes a Coq module (a bit like OCaml files
become OCaml modules). So myFile.v will become the
myFile module, and those don’t allow for dashes in them. In
fact, it’s better to stick to letters and underscores
(_).
Note
There’s no need to understand all this, just know that if Coq won’t even start then it’s a good idea to try for a simpler name, just in case.
If you want to know how long a tactic or a command takes, you can use
the Time
command for instance as follows:
Time my_tactic.Yes, possibly before the end of the course, Coq should be renamed to Rocq. Officially it’s still called Coq, but people have already starting using the new name.
Nix can be used to install Coq and Equations, as well as many other
packages, but it seems to be currently broken when it comes to MetaCoq
so unless you want to spend hours debugging things, we recommend you use
opam or the binary installers as advised in the installation page.
If simpl simplifies too much, you can also use
eg. simpl add to only simplify addition. So for
instance (0 + S n) - m will become S n - m
without Coq unfolding also -.
You will see in lesson 3 a bit more about computation and how to control it.