diff options
| author | Maxime Dénès | 2018-05-16 15:25:07 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-05-16 15:25:07 +0200 |
| commit | 19e24bf1f5eefee37ee2648c04844b5ea3ca2ab2 (patch) | |
| tree | 60ae3d8527f10aa5e198639139364bdaebddf821 /doc/sphinx/addendum | |
| parent | 3f480c993311d19b152deb6bb4dc561188d76fc7 (diff) | |
| parent | e266976abc8c170c1e4bf1c98629c190b844f1ab (diff) | |
Merge PR #7391: Add a small documentation writer's guide
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/implicit-coercions.rst | 22 | ||||
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 5 |
2 files changed, 14 insertions, 13 deletions
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index 152f4f6552..09faa06765 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -140,29 +140,29 @@ Declaration of Coercions .. warn:: Ambiguous path. - When the coercion `qualid` is added to the inheritance graph, non - valid coercion paths are ignored; they are signaled by a warning - displaying these paths of the form :g:`[f₁;..;fₙ] : C >-> D`. + When the coercion :token:`qualid` is added to the inheritance graph, non + valid coercion paths are ignored; they are signaled by a warning + displaying these paths of the form :g:`[f₁;..;fₙ] : C >-> D`. .. cmdv:: Local Coercion @qualid : @class >-> @class - Declares the construction denoted by `qualid` as a coercion local to - the current section. + Declares the construction denoted by `qualid` as a coercion local to + the current section. .. cmdv:: Coercion @ident := @term - This defines `ident` just like ``Definition`` `ident` ``:=`` `term`, - and then declares `ident` as a coercion between it source and its target. + This defines `ident` just like ``Definition`` `ident` ``:=`` `term`, + and then declares `ident` as a coercion between it source and its target. .. cmdv:: Coercion @ident := @term : @type - This defines `ident` just like ``Definition`` `ident` : `type` ``:=`` `term`, - and then declares `ident` as a coercion between it source and its target. + This defines `ident` just like ``Definition`` `ident` : `type` ``:=`` `term`, + and then declares `ident` as a coercion between it source and its target. .. cmdv:: Local Coercion @ident := @term - This defines `ident` just like ``Let`` `ident` ``:=`` `term`, - and then declares `ident` as a coercion between it source and its target. + This defines `ident` just like ``Let`` `ident` ``:=`` `term`, + and then declares `ident` as a coercion between it source and its target. Assumptions can be declared as coercions at declaration time. This extends the grammar of assumptions from diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index f887a5feea..0e9c23b9bb 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -150,9 +150,10 @@ are a way to take into account the discreteness of :math:`\mathbb{Z}` by roundin .. _ceil_thm: -**Theorem**. Let :math:`p` be an integer and :math:`c` a rational constant. Then +.. thm:: Bound on the ceiling function - :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil` + Let :math:`p` be an integer and :math:`c` a rational constant. Then + :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil`. For instance, from 2 x = 1 we can deduce |