aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/language/cic.rst
AgeCommit message (Collapse)Author
2021-04-10Fix link in doc/cic.rst, there is no Credits chapter anymoreYannick Forster
2021-03-08Convert 2nd part of rewriting chapter to prodnJim Fehrle
2020-12-30Convert rewriting and proof-mode chapters to prodnJim Fehrle
2020-11-09[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.Théo Zimmermann
The smallcaps rendering was inexistent in the PDF version and did not look good in the HTML version.
2020-09-30Type{i} should be Type(i).Tanaka Akira
2020-05-14Reintroduce leftover parts; update index files; small fixes.Théo Zimmermann
2020-05-13Preserve sections about typing rules in CIC chapter.Théo Zimmermann
2020-05-07Drop some the coqtop output, rephrase a bitQuentin Carbonneaux
2020-05-06Add an example to motivate strictly positive occurrences checkQuentin Carbonneaux
2020-05-01Move essential vocabulary and syntax conventions to section on basics.Théo Zimmermann
2020-03-26Remove outdated mention of -allow-sprop.Théo Zimmermann
2020-03-19Document all the existing attributes.Théo Zimmermann
And fix documentation following the removal of the Template Check flag in #11546.
2019-11-14Fix doc for universes(foo) attributesGaëtan Gilbert
Fix #10570
2019-11-08Merge PR #11050: Replace "option" in doc when it refers to a flagThéo Zimmermann
Reviewed-by: Zimmi48
2019-11-06Replace "option" in doc when it refers to a flagJim Fehrle
2019-11-04Cite POPL19 SProp paperGaëtan Gilbert
Close #10242
2019-10-30Use bullets and indentation (but the result rendering is weird).Théo Zimmermann
2019-10-30Use explicit match as suggested by Clément.Théo Zimmermann
2019-10-30[refman] Add a second example of contradiction when positivity checking is ↵Théo Zimmermann
disabled.
2019-10-30[refman] Give an example of contradiction when positivity checking is disabled.Théo Zimmermann
2019-10-22documentation fixesAntonio Nikishaev
document « Property » more documentation fixes [doc] destructed → destructured [doc] another le_minus→lt_1_r [doc] @jfehrle suggestions [doc] more minor fixes
2019-08-26Document `Template Check` flag and add changelog entry for 9918Matthieu Sozeau
Fix changelog entry Fix build of the user manual Markup fixes from Théo Zimmermann Update doc and changelog and improve error messages.
2019-03-14Documentation for SPropGaëtan Gilbert
2019-02-20Merge PR #9457: Correct W-Ind in Cic description of the reference manual.Théo Zimmermann
Reviewed-by: SkySkimmer
2019-02-19Make the conclusion of local contexts W-Ind empty.Tanaka Akira
The conclusion of W-Ind, "\WF{E;~\ind{p}{Γ_I}{Γ_C}}{Γ}", is changed to "\WF{E;~\ind{p}{Γ_I}{Γ_C}}{}" because local contexts should be empty when inductive definition is defined globally. This is consistent with W-Global-Assum and W-Global-Def. The side condition "c_i ∉ Γ ∪ E" which I changed previous commit is changed again to "c_i ∉ E" because I guess that it tries to avoid name conflicts to the local contexts in the conclusion. However, the condition is useless after the local contexts is empty.
2019-02-13Merge PR #9564: Fix small errors in cic.rst (3rd)Théo Zimmermann
Reviewed-by: Zimmi48
2019-02-12Fix failing coqtops in cic.rstGaëtan Gilbert
2019-02-11Use math mode more.Tanaka Akira
Also quoted parts are emphasized as coq-8.7.2-reference-manual.pdf. And two "x:T" are quoted.
2019-02-11Use {LEFT,RIGHT} DOUBLE QUOTATION MARK.Tanaka Akira
Use LEFT DOUBLE QUOTATION MARK (U+201C) and RIGHT DOUBLE QUOTATION MARK (U+201D) instead of QUOTATION MARK (U+0022). QUOTATION MARK is formatted as same form both for opening and closing quotation mark.
2019-02-11Remove a space before closing double-quote.Tanaka Akira
2019-02-10Change "I" to "I_p".Tanaka Akira
Since the type of "c" is "I_p ...", the constructor should return the value of it.
2019-02-10Distinguish inductive {definition,inductive}.Tanaka Akira
2019-02-08Use math mode more.Tanaka Akira
2019-02-08Fix index of arguments of constructor in fixpoint.Tanaka Akira
In fixpoint typing rule section, a type of constructor is described twice: - ∀ p_1:P_1,~… ∀ p_r :P_r,~∀ x_1:T_1,~… ∀ x_r:T_r,~(I_j~p_1 … p_r~t_1 … t_s) - ∀ p_1:P_1,~…,∀ p_r :P_r,~∀ y_1:B_1,~… ∀ y_k:B_k,~(I~a_1 … a_k) Both seems invalid. The former require that the number of parameters and the number of (non-parameter) constructor argumets is same. The latter require that the number of (non-parameter) constructor argumets and the number of inductive type arguments (including paramters) is same. Also, "k" is already used for the number of inductive types in a inductive definition. So, I changed the number of (non-parameter) constructor argumets to "m". I choose "m" because "m" is used for the purpose in the description for iota-reduction of destructors. Also, I changed the inductive type parameters and arguments of latter consistent with the former.
2019-02-08Change parameters p_1...p_r to q_1...q_r.Tanaka Akira
In the description of destructors, "Type of branches" section and "Typing rule" section shares the definition of "r" (and "s" from previous commit). However actual parameters are p_1...p_r in the former section and q_1...q_r in the latter section. I guess it's because the latter section uses p_1...p_l in other purpose: index of constructor for a inductive type. So, I change the parameter p_1...p_r to q_1...q_r in the former section to consistent with the latter section.
2019-02-08Change the index "p" to "s" in "type of branches".Tanaka Akira
In the description of destuctors, "Type of branches" section uses "p" as the number of arguments. It is confusing because "p" is used as the number of parameters. After the section, "Typing rule." section uses "s" without definition as I q1...qr t1...ts. It seems that it is the number of arguments. So, I changed "p" to "s". "s" is also confusing with sorts, though.
2019-02-08Change c to c' forgotten at exchanging c and c'.Tanaka Akira
In Cic admissible rules section, c and c' are exchanged at https://github.com/coq/coq/commit/8654b03544f0efe4b418a0afdc871ff84784ff83 . But the exchange is not complete. This commit complete it.
2019-02-08Remove spaces just before period (non-math mode).Tanaka Akira
2019-02-08Remove spaces just before comma (non-math mode).Tanaka Akira
2019-02-08Remove "'" accidentaly added.Tanaka Akira
"'" in the extended (k_i added) form of Fix syntax should be removed. In the following sentence, A_i' is referenced as A_i. ``` Each :math:`A_i` should be a type (reducible to a term) starting with at least :math:`k_i` products :math:`∀ y_1 :B_1 ,~… ∀ y_{k_i} :B_{k_i} ,~A_i'` ``` Also, A_i' is used in ∀ y_1 :B_1 ,~… ∀ y_{k_i} :B_{k_i} ,~A_i' and A_i' must not equal to ∀ y_1 :B_1 ,~… ∀ y_{k_i} :B_{k_i} ,~A_i'. The old reference manual, coq-8.7.2-reference-manual.pdf, doesn't have "'". They are added by https://github.com/coq/coq/commit/47dca6c5da585212f69b6b83b25896ff990781e3 which ports Cic document from TeX to sphinx. So, the change seems just an accident.
2019-02-01Correct W-Ind.Tanaka Akira
Remove the 2nd premise "(E[Γ_P ] ⊢ A_j : s_j)_(j=1...k)". Also, "Γ" in "c_i ∉ Γ ∪ E" is changed to "Γ_I". "E[Γ_P ] ⊢ A_j : s_j" contradicts with a side condition "A_j is an arity of sort s_j". The latter means that A_j is ∀ x1:T1, ... ∀ xm:Tm, s_j. So, "(∀ x1:T1, ..., s_j) : s_j)" is required. Using Prod-{Prop,Set,Type}, it needs "s_j : s_j" which cannot be proved. This problem is introduced at 2018-07-22: https://github.com/coq/coq/commit/f25c1d252ad61b4dc4321e3a11f33b1e6d4e3dff Before that, the premise describes "A_j : s'_j". And "s'_j" is not explained anywhere. I think "A_j : s'_j" describes that A_j is a type (a value of a sort). Thus, "A_j is an arity of sort s_j" imply "A_j : s'_j". So, I removed the 2nd premise. Also, a side condition describes "c_i ∉ Γ ∪ E" but "Γ" is not explained. I think that Γ should be Γ_I. Γ should include Γ_I because a constructor, c_i, and inductive types are both defined in global environment and it cannot accept duplicate name. Actually, such definition fails: ``` Fail Inductive X := X : X. (* The following names are used both as type names and constructor names: X.*) ``` Γ doesn't include Γ_P because parameters are not defined in global environment. Actually, a parameter can be same name as a constructor name: ``` Inductive I (X : nat) := X : I X. Check X. (* X : forall X : nat, I X *) ```
2019-02-01The lowest universe level is 1.Tanaka Akira
Cic description doesn't describe the lowest universe level clearly. - "Type(i) for any integer i" seems Type(-1) is possible - "S = {Prop,Set,Type(i)| i ∈ ℕ }" depends on the definition of "ℕ" which is not described. It is well known that there are two definitions that ℕ includes 0 or not. In Coq, it is natural that ℕ includes 0 because the inductive type nat includes 0. - "Prop:Type(1), Set:Type(1)" suggests the lowest level is 1. - AX-Prop and AX-Set describes Prop:Type(1) and Set:Type(1). So, Prop and Set are not belongs to Type(0). Also, CPDT describes that "The type of Set is Type(0)". http://adam.chlipala.net/cpdt/html/Universes.html I think the lowest universe level is 1 because AX-Prop and AX-Set. I'm not certain to fix this problem but my idea to fix this problem is changing "Type(i) for any integer i" to "Type(i) for any integer i ≥ 1".
2019-01-31Use λ instead of \lb.Tanaka Akira
The former is more succinct and intuitive.
2019-01-31The subst Γ{c}{(c c')} should be Γ{c'}{(c' c)}.Tanaka Akira
c can be non-function since c:U. So, c c' is not typeable.
2019-01-31Use "U" instead of "u" for a type.Tanaka Akira
2019-01-31Fix an index. The number of constructors is "l".Tanaka Akira
2019-01-31Use \Match for match construct.Tanaka Akira
2019-01-31Insert a space before \kwend.Tanaka Akira
2019-01-31Use \length for the function name of length.Tanaka Akira
2019-01-31Adjust spaces.Tanaka Akira
This commit basically ajusts spaces as - ∀x:T,t to ∀x:T,~t - λx:T.t to λx:T.~t - E;c:T to E;~c:T x and T are more related than T and t. So, T and t should not positioned closely than x and T. Unfortunately, they are formatted that T and t are positioned closely without "~". (Similary, c and T are more related than E and c.)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:19:36 +0000