diff options
| author | Pierre-Marie Pédrot | 2020-03-20 15:52:42 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-20 15:52:42 +0100 |
| commit | 4d025d4161599ea20cd1dbf489a6412f019a7a7e (patch) | |
| tree | 9374846f74bc76efe4c4f3e8f5ffd7840014af5c /doc/sphinx/addendum/program.rst | |
| parent | 5b7a6471cf812a708dbbb8943f30d525e46250f6 (diff) | |
| parent | 4b37834a2ed6a275daec1c98fac19795f96712ce (diff) | |
Merge PR #11665: Make Cumulative, NonCumulative and Private attributes.
Ack-by: SkySkimmer
Reviewed-by: jfehrle
Reviewed-by: ppedrot
Diffstat (limited to 'doc/sphinx/addendum/program.rst')
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 549249d25c..cbb5c0db8a 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -98,10 +98,17 @@ coercions. .. flag:: Program Mode Enables the program mode, in which 1) typechecking allows subset coercions and - 2) the elaboration of pattern matching of :cmd:`Program Fixpoint` and - :cmd:`Program Definition` act - like Program Fixpoint/Definition, generating obligations if there are - unresolved holes after typechecking. + 2) the elaboration of pattern matching of :cmd:`Fixpoint` and + :cmd:`Definition` act as if the :attr:`program` attribute had been + used, generating obligations if there are unresolved holes after + typechecking. + +.. attr:: program + + This attribute allows to use the Program mode on a specific + definition. An alternative syntax is to use the legacy ``Program`` + prefix (cf. :n:`@legacy_attr`) as documented in the rest of this + chapter. .. _syntactic_control: |