In Ilya Sergey's Programs and Proofs, ssrnat's command .+1 is introduced and used for defining some functions on the natural numbers. Although its usage is well explained there, I'm also interested in how it is defined and, more importantly, how it works. Earlier in that chapter the nat type is introduced, which we can verify the definition with "Print nat.", which yields:
Inductive nat : Set := O : nat | S : nat -> nat
For .+1 however, the commands "Print .+1." or "Print +1." yield:
Syntax error: 'Fields' or 'Rings' or 'Hint' 'View' expected after 'Print' (in [command]).
Even trying to circumvent this by adding a natural number before it, such as in "Definition one: nat := 1." followed by "Print one.+1." yields:
Syntax error: '.' expected after [command] (in [vernac_aux]).
However, I imagine this command is defined in the library and is not a primitive of the language, so it feels like one should be able to examine its definition as any other.
If that's the case, why is the command not working and how may the definition of .+1 be printed?
Note: In case that is impossible, an explanation of why is also acceptable as an answer (and a resource for the code/workings of the command appreciated).
To print a notation such as
.+1you have to use quotation marks.If you do so you will end up with the same result as
Print nat.because that's what happens when you print a constructor of an inductive type. In fact you get the result ofPrint S.because.+1is a notation for it.For notations, usually you want to use
Locate:And this time the output is more informative:
A notation, is not the same as a definition. It's just a way to write and print an expression, but underneath it's the same.
To clarify,
.+1is a notation, not a command. Commands are things such asDefinition,Printetc. I encourage you to have a look at the documentation if you want to know more about those.