| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: maximedenes
|
|
Coq and the Coq libraries can now be excluded
(by setting the NOCOQ environment variable).
|
|
|
|
|
|
|
|
Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: mattam82
Ack-by: ppedrot
|
|
Reviewed-by: ejgallego
|
|
|
|
\nO, \nS, \evenO, \evenS, \oddS, \length, \Nil and \cons are used.
don't use \kw in \kw{n} in Fixpoint typing rule section.
|
|
Fix small errors in cic.rst:
* 3.4.1 Free variables: use :math: for "∀ x:T,~U".
:g: doesn't show "∀" in PDF.
"λx:T.~U" is also changed to :math: to use consistent font.
* 3.4.3 Zeta: ":U" added in "let x:=u:U in t" to be valid let-in expression.
* 3.4.3 convertibility: add :math: for u_2' to apply math formatting.
* 3.4.4.6: fix index. "n" should be "k" because they corresponds k-th
constructor.
* 3.4.5 Type constructor: I changed the section title "Type constructor" to
"Type of constructor".
"Type constructor" means a feature to construct new type.
But this section describes about a type of constructor.
* 3.4.5 Example nattree: The reason of
"``nattree`` occurs only strictly positively in ``A``" should be
bullet 1 instead of bullet 3.
The bullet 3 of strict positivity definition is about product, "∀x ∶ U , V",
but "A" is not a product.
* 3.4.5 Destructors: use :math: for "∀".
:g: doesn't show "∀" in PDF.
Also, :math: is used for expressions which has no "∀" character
for font consistency.
Note that I use \kw{has}\_\kw{length} instead of
\kw{has\_length} because the latter is formatted as has\_length in HTML.
(the backslash is retained.)
* 3.4.5 list example: curly braces added.
* 3.4.5 Fixpoint definition: add :math: for Γ_i to apply math formatting.
* 3.4.6 2nd rule of First abstracting property: use \subst.
This adds a curly brace.
Also, spacing and fonts are adjusted as follows.
* 3.4.1 let-in term: use :math: for variable x, consistent with other term
descriptions.
* 3.4.1 let-in term: use \letin command for concrete let-in term.
* 3.4.2 Note: insert spaces as ((λ x:T.~u)~t).
Since T is more closely reated to x than u, T should be positioned
close to x than u.
Since it seems most application has a space, I inserted a space here
for consistency.
* 3.4.3 beta-reduction: insert spaces as 3.4.2.
* 3.4.3 eta-expansion: insert spaces as 3.4.2.
* 3.4.5 Example: use sans-serif fonts for constructor "O" and "S".
* 3.4.5 Fixpoint definition: insert spaces around "with".
* 3.4.5 Fixpoint typing rule: fix fonts for "O" and "S" as 3.4.5 and
insert spaces as 3.4.2.
* 3.4.5 Fixpoint reduction rule: insert a space between {F} and a_1 for
consistency.
* 3.4.6 First abstracting property: insert spaces as 3.4.2.
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: MSoegtropIMC
|
|
Ack-by: SkySkimmer
Ack-by: maximedenes
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
|
|
an error
Ack-by: maximedenes
Reviewed-by: ppedrot
|
|
computed
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
Reviewed-by: gares
|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
|
|
suite again
|
|
|
|
Reviewed-by: maximedenes
|
|
|
|
This makes the implementation of Timeout on unix more reliable
since only the main thread will receive the signal for
timeout.
|
|
Was raising an anomaly 'Failure("Grammar.extend")' otherwise.
|
|
Reviewed-by: ejgallego
|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
|
|
Using a unit test as it's way faster than messing with universes.
You can test with universes by
~~~coq
Set Universe Polymorphism.
Definition x1@{i} := True.
Definition x2 := x1 -> x1.
Definition x3 := x2 -> x2.
Definition x4 := x3 -> x3.
Definition x5 := x4 -> x4.
Definition x6 := x5 -> x5.
Definition x7 := x6 -> x6.
Definition x8 := x7 -> x7.
Definition x9 := x8 -> x8.
Definition x10 := x9 -> x9.
Definition x11 := x10 -> x10.
Definition x12 := x11 -> x11.
Definition x13 := x12 -> x12.
Definition x14 := x13 -> x13.
Definition x15 := x14 -> x14.
Definition x16 := x15 -> x15.
Definition x17 := x16 -> x16.
Definition x18 := x17 -> x17.
Definition x19 := x18 -> x18.
About x19. (* 262144 universes *)
~~~
Note on my machine `About x18.` did not overflow even before this
commit.
|
|
|
|
|
|
|
|
This makes code paths clearer (we still factorize a lot of the
treatment), and we seize the opportunity to forbid anonymous
`Declare Instance` which is not a documented construction, and seems to
make little sense in practice.
|
|
|
|
|
|
|
|
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: mattam82
Ack-by: maximedenes
Ack-by: ppedrot
|
|
|
|
|
|
We split into smaller functions, use more specific types for universe
manipulation, and try to limit how much of the big tuple gets passed
to subroutines.
|
|
This is strictly code movement.
|
|
|
|
This error was more or less a debug tool (checking that no tactic breaks
the invariant). But some users may want to support other models, see
https://github.com/Mtac2/Mtac2/pull/139 for an example discussion.
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: mattam82
Reviewed-by: maximedenes
|
|
Reviewed-by: maximedenes
|
|
Reviewed-by: maximedenes
|
|
ML files at the root were not taken into account. Coqdep was already
doing the right thing.
|
