diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index e7db9cfaca..e866e4c624 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1152,6 +1152,12 @@ Controlling Typing Flags anymore but it still affects the reduction of the term. Unchecked fixpoints are printed by :cmd:`Print Assumptions`. +.. attr:: bypass_check(guard{? = {| yes | no } }) + :name: bypass_check(guard) + + Similar to :flag:`Guard Checking`, but on a per-declaration + basis. Disable guard checking locally with ``bypass_check(guard)``. + .. flag:: Positivity Checking This flag can be used to enable/disable the positivity checking of inductive @@ -1159,6 +1165,12 @@ Controlling Typing Flags break the consistency of the system, use at your own risk. Unchecked (co)inductive types are printed by :cmd:`Print Assumptions`. +.. attr:: bypass_check(positivity{? = {| yes | no } }) + :name: bypass_check(positivity) + + Similar to :flag:`Positivity Checking`, but on a per-declaration basis. + Disable positivity checking locally with ``bypass_check(positivity)``. + .. flag:: Universe Checking This flag can be used to enable/disable the checking of universes, providing a @@ -1167,6 +1179,12 @@ Controlling Typing Flags :cmd:`Print Assumptions`. It has the same effect as `-type-in-type` command line argument (see :ref:`command-line-options`). +.. attr:: bypass_check(universes{? = {| yes | no } }) + :name: bypass_check(universes) + + Similar to :flag:`Universe Checking`, but on a per-declaration basis. + Disable universe checking locally with ``bypass_check(universes)``. + .. cmd:: Print Typing Flags Print the status of the three typing flags: guard checking, positivity checking |