diff options
| author | Maxime Dénès | 2018-08-16 15:46:45 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-08-16 15:46:45 +0200 |
| commit | 6fe61aacc57e82de491debb544844c41b1f27757 (patch) | |
| tree | 86479a0f0d3f07bcde3ee5c83c457e98097840b2 | |
| parent | 07c25cfaea5f4f97f2a763a58ce80207a948365c (diff) | |
| parent | 80883ddf89949afa82081ba80ccb4934320e6ee3 (diff) | |
Merge PR #8111: Docs: Fix p values in CIC Inductive Defs examples
| -rw-r--r-- | doc/sphinx/language/cic.rst | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 6e0c1e1b61..a63400103f 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -747,7 +747,7 @@ the sort of the inductive type t (not to be confused with :math:`\Sort` which is is: .. math:: - \ind{~}{\left[\begin{array}{rcl}\tree&:&\Set\\\forest&:&\Set\end{array}\right]} + \ind{0}{\left[\begin{array}{rcl}\tree&:&\Set\\\forest&:&\Set\end{array}\right]} {\left[\begin{array}{rcl} \node &:& \forest → \tree\\ \emptyf &:& \forest\\ @@ -769,7 +769,7 @@ the sort of the inductive type t (not to be confused with :math:`\Sort` which is The declaration for a mutual inductive definition of even and odd is: .. math:: - \ind{1}{\left[\begin{array}{rcl}\even&:&\nat → \Prop \\ + \ind{0}{\left[\begin{array}{rcl}\even&:&\nat → \Prop \\ \odd&:&\nat → \Prop \end{array}\right]} {\left[\begin{array}{rcl} \evenO &:& \even~0\\ @@ -966,7 +966,7 @@ such that :math:`Γ_I` is :math:`[I_1 :∀ Γ_P ,A_1 ;…;I_k :∀ Γ_P ,A_k]`, .. inference:: W-Ind \WFE{Γ_P} - (E[Γ_P ] ⊢ A_j : s_j' )_{j=1… k} + (E[Γ_P ] ⊢ A_j : s_j )_{j=1… k} (E[Γ_I ;Γ_P ] ⊢ C_i : s_{q_i} )_{i=1… n} ------------------------------------------ \WF{E;\ind{p}{Γ_I}{Γ_C}}{Γ} @@ -1025,7 +1025,7 @@ Template polymorphism +++++++++++++++++++++ Inductive types declared in :math:`\Type` are polymorphic over their arguments -in :math:`\Type`. If :math:`A` is an arity of some sort and math:`s` is a sort, we write :math:`A_{/s}` +in :math:`\Type`. If :math:`A` is an arity of some sort and :math:`s` is a sort, we write :math:`A_{/s}` for the arity obtained from :math:`A` by replacing its sort with :math:`s`. Especially, if :math:`A` is well-typed in some global environment and local context, then :math:`A_{/s}` is typable by typability of all products in the |