diff options
Diffstat (limited to 'doc/sphinx/proof-engine/vernacular-commands.rst')
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 001bacc9ec..342425567e 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1250,3 +1250,17 @@ Inlining hints for the fast reduction machines Due to its internal nature, this command is not for general use. It is meant to appear only in standard libraries and in support libraries of plug-ins. + +Registering primitive operations +-------------------------------- + +.. cmd:: Primitive @ident__1 := #@ident__2. + + Declares :n:`@ident__1` as the primitive operator :n:`#@ident__2`. When + running this command, the type of the primitive should be already known by + the kernel (this is achieved through this command for primitive types and + through the :cmd:`Register` command with the :g:`kernel` name-space for other + types). + + Due to its internal nature, this command is not for general use. It is meant + to appear only in standard libraries and in support libraries of plug-ins. |