diff options
| author | Théo Zimmermann | 2020-11-14 18:44:57 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-11-18 16:25:00 +0100 |
| commit | ca42305f1ed1699065cffdef7d96bf5fcc0069be (patch) | |
| tree | b72fb82071db98d6ab2c1b52f22e57e1c1befc9f /doc/sphinx/addendum/program.rst | |
| parent | 3b479357d8c5c1a655b2b8257f14a8cafe7621fc (diff) | |
Review commit: improving the doc of boolean attributes.
Diffstat (limited to 'doc/sphinx/addendum/program.rst')
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 298ea4b4ab..104f84a253 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -99,15 +99,15 @@ coercions. Enables the program mode, in which 1) typechecking allows subset coercions and 2) the elaboration of pattern matching of :cmd:`Fixpoint` and - :cmd:`Definition` act as if the :attr:`program` attribute had been + :cmd:`Definition` acts as if the :attr:`program` attribute has been used, generating obligations if there are unresolved holes after typechecking. -.. attr:: program +.. attr:: program{? = {| yes | no } } :name: program; Program - Allows using the Program mode on a specific - definition. An alternative syntax is to use the legacy ``Program`` + This :term:`boolean attribute` allows using or disabling the Program mode on a specific + definition. An alternative and commonly used syntax is to use the legacy ``Program`` prefix (cf. :n:`@legacy_attr`) as it is elsewhere in this chapter. .. _syntactic_control: |