aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
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-06Merge PR #9124: Document the possibility of declaring a Ltac name_goal.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-02-06Merge PR #9456: The lowest universe level is 1.Théo Zimmermann
Reviewed-by: Zimmi48
2019-02-06Document the possibility of declaring a Ltac name_goal.Théo Zimmermann
2019-02-05Documenting the Ltac Backtrace flag.Pierre-Marie Pédrot
2019-02-05Add advice and an example to the documentation of fold.Théo Zimmermann
2019-02-04Primitive integersMaxime Dénès
This work makes it possible to take advantage of a compact representation for integers in the entire system, as opposed to only in some reduction machines. It is useful for heavily computational applications, where even constructing terms is not possible without such a representation. Concretely, it replaces part of the retroknowledge machinery with a primitive construction for integers in terms, and introduces a kind of FFI which maps constants to operators (on integers). Properties of these operators are expressed as explicit axioms, whereas they were hidden in the retroknowledge-based approach. This has been presented at the Coq workshop and some Coq Working Groups, and has been used by various groups for STM trace checking, computational analysis, etc. Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr> Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr> Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
2019-02-01Merge PR #8062: Add Z.div_mod_to_quot_rem tactic, put it in zifyVincent Laporte
Ack-by: JasonGross Reviewed-by: fajb Reviewed-by: jfehrle
2019-02-01Merge PR #9095: [toplevel] Deprecate `-compile` flag in favor of `coqc`Maxime Dénès
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: ejgallego Ack-by: gares Reviewed-by: maximedenes
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.)
2019-01-31Use "∀" and "λ" instead of \forall and \lambda.Tanaka Akira
The former is more succinct and consistent with most of other parts in cic.rst.
2019-01-31Use math more.Tanaka Akira
Add :math:`...` for mathematical expressions.
2019-01-31Make parenthesis correctly matched.Tanaka Akira
2019-01-31\Sort is not a term.Tanaka Akira
"∀Γ_P ,∀Γ_{\mathit{Arr}(t)}, \Sort" is changed to "∀Γ_P ,∀Γ_{\mathit{Arr}(t)}, S" because \Sort is not a term. "S" is choosen to be consistent with the description of Inductive Definitions.
2019-01-31Use semicolon for separator of local contexts.Tanaka Akira
2019-01-31Don't line break at hyphen of compound words.Tanaka Akira
2019-01-31Move out a period and comma from :math:.Tanaka Akira
2019-01-31Nest :math: and parenthesis properly.Tanaka Akira
Exchange a closing parenthesis and a :math: closing backquote.
2019-01-31Fix syntax of two lambda-abstractions.Tanaka Akira
In the note about η-reduction, two lambda-abstraction used "," instead of ".".
2019-01-31Change {\Sort} to \Sort.Tanaka Akira
After #9435 (Use \mathcal instead of \cal), \Sort doesn't have font changing effect. So, {\Sort} is same as \Sort now and the former is changed to latter in cic.rst.
2019-01-31Use \Prop, \Set and \Type defined in refman-preamble.sty.Tanaka Akira
2019-01-31Make "1" and "2" in "f1" and "f2" suffixes.Tanaka Akira
2019-01-31Make "1" and "n" in "u1" and "un" suffixes.Tanaka Akira
2019-01-31Remove "End TreeExample." line.Tanaka Akira
This corresponds to "Module TreeExample." removed at 2018-04-24 bcf5352cc7a26a672e719f7dad4021c69d723833.
2019-01-31Merge PR #8720: [Numeral notations] Use Coqlib registered constantsEmilio Jesus Gallego Arias
Reviewed-by: JasonGross Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: ppedrot Ack-by: vbgl
2019-01-30[toplevel] Deprecate the `-compile` flag in favor of `coqc`.Emilio Jesus Gallego Arias
This PR deprecates the use of `coqtop` as a compiler. There is no point on having two binaries with the same purpose; after the experiment in #8690, IMHO we have a lot to gain in terms of code organization by splitting the compiler and the interactive binary. We adapt the documentation and adapt the test-suite. Note that we don't make `coqc` a true binary yet, but here we take care only of the user-facing part. The conversion of the binary will take place in #8690 and will bring code simplification, including a unified handling of arguments.
2019-01-29Use \mathcal instead of \calGaëtan Gilbert
Apparently it's deprecated / doesn't always work, see https://tex.stackexchange.com/questions/84041/why-does-calm-n-give-m See #9429 (we also need to fix the distributed file on the server).
2019-01-28Surround "assumption" with :tacn:`` in tactics.rstRyan Scott
2019-01-28Merge PR #9402: Move \def\plus and \def\tri to refman-preamble.sty.Théo Zimmermann
Reviewed-by: Zimmi48
2019-01-28Merge PR #9341: [ssr] uniform clear disciplineMaxime Dénès
Reviewed-by: CohenCyril Ack-by: Zimmi48 Ack-by: gares Reviewed-by: maximedenes
2019-01-25Merge PR #9391: Clarify meaning of Primitive ProjectionsThéo Zimmermann
Reviewed-by: Zimmi48
2019-01-25[Numeral notations] Lazy resolution of decimal typesVincent Laporte
2019-01-24Rename Z.div_mod_to_quot_rem, add Z.quot_rem_to_equations, ↵Jason Gross
Z.to_euclidean_division_equations
2019-01-24Revert "Add subst to the end of nia in the test-suite"Jason Gross
This reverts commit b49f4e966443a76ac70d37c4cde68f94de164c01. It turns out the 4x was due to .nia.cache (because I didn't clean sufficiently in testing), not due to `subst`.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 04:41:43 +0000