diff options
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 |