| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
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
|
|
|
|
Ack-by: Zimmi48
Reviewed-by: gares
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: gares
Ack-by: mattam82
|
|
Reviewed-by: cpitclaudel
|
|
records
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
Reviewed-by: mattam82
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: gares
Ack-by: maximedenes
Ack-by: ppedrot
|
|
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: SkySkimmer
Reviewed-by: ejgallego
|
|
|
|
In order for Dune to work in Windows we need to tweak some script
calls, they need a POSIX shell and the `(run ...)` / `(system ...)`
actions use `cmd.exe` on Windows.
Hopefully, we will rely less on `bash` when Dune can understand Coq
libraries. This affects shell scripts in `kernel/**.sh` for example.
It is interesting to see how faster the Coq Windows build is with Dune
+ Windows.
There are some problems with PATHs that prevent the test suite from
working, these will be fixed in a future PR.
|
|
|
|
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot
|
|
Ack-by: SkySkimmer
Reviewed-by: mattam82
Reviewed-by: ppedrot
|
|
Ack-by: herbelin
Reviewed-by: ppedrot
|
|
declare_mutual_inductive_with_eliminations
Reviewed-by: ppedrot
|
|
Reviewed-by: mattam82
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
Reviewed-by: herbelin
Reviewed-by: ppedrot
|
|
|
|
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>
|
|
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
Reviewed-by: maximedenes
Ack-by: ppedrot
|
|
Reviewed-by: gares
|
|
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: fajb
|
|
Ack-by: mattam82
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
|
|
Ack-by: JasonGross
Reviewed-by: fajb
Reviewed-by: jfehrle
|
|
We make `coqc` a truly standalone binary, whereas `coqtop` is
restricted to interactive use.
Thus, `coqtop -compile` will emit a warning and call `coqc`.
We have also refactored `Coqargs` into a common `Coqargs` module and a
compilation-specific module `Coqcargs`.
This solves problems related to `coqc` having its own argument
parsing, and reduces the number of strange argument combinations a
lot.
|
|
Ack-by: JasonGross
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: tchajed
|
|
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".
|
