| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: Zimmi48
|
|
Ack-by: Zimmi48
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Mostly in the pattern
~~~
.. coqtop:: in
Theorem foo : bla.
Theorem bar : blah. (* nested proof error *)
~~~
|
|
|
|
|
|
In particular, mention that auto does not use full-blown apply.
|
|
|
|
Maybe we should still let it run but let's disable it until we install
csdp on the build server at least.
|
|
|
|
|
|
|
|
Not sure why but it seems required for future commits.
|
|
|
|
Also quoted parts are emphasized as coq-8.7.2-reference-manual.pdf.
And two "x:T" are quoted.
|
|
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.
|
|
|
|
Since the type of "c" is "I_p ...", the constructor should
return the value of it.
|
|
|
|
|
|
|
|
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.
|
|
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.
|
|
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.
|
|
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.
|
|
|
|
|
|
"'" 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.
|
|
Reviewed-by: cpitclaudel
|
|
Reviewed-by: Zimmi48
|
|
|
|
|
|
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>
|
|
Ack-by: JasonGross
Reviewed-by: fajb
Reviewed-by: jfehrle
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: maximedenes
|
|
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".
|
|
The former is more succinct and intuitive.
|
|
c can be non-function since c:U.
So, c c' is not typeable.
|
|
|
|
|
|
|
|
|
|
|
|
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.)
|
