| Age | Commit message (Collapse) | Author |
|---|
|
Documentation of FieldUnitMixin and FieldMixin corrected to reflect
actual arguments, with mulVf and inv0 made explicit arguments for
FieldMixin (they were implicit due to the extended signature of
Field.mixin_of). Type of FieldMixin changed to a convertible variant to
facilitate construction of on-the-fly in-proof construction of
fieldType instances, exposing an idomainType instance.
|
|
See the discussion here:
https://github.com/math-comp/math-comp/pull/242#discussion_r233778114
|
|
Remove some unused canonical mixins.
Change simplification behavior of concrete comparison functions to allow for
better simplification using unfolding and sebsequent folding back e.g. with
`rewrite !eqE /= -!eqE`.
A bit of cleanup for `Prenex Implicits` declarations.
Document some explanations by G. Gonthier.
|
|
Adding missing documentation for mixin and class constructors for
Equality, Choice, Countable, and Finite.
Renaming Equality mixin constructor comparableClass to the more
consistent comparableMixin.
|
|
should fix #238
|
|
This reverts commit 044634dcc2f645e3afbdad6cb8dcc66f3eb4a87e.
See issue https://github.com/math-comp/odd-order/pull/5
|
|
fix some bugs in Makefile
|
|
Statement of `bool_irrelevance` more consistent with its name.
|
|
|
|
|
|
- countalg goes to the algebra package
- finalg now get the expected inheritance from countalg
- closed_field now contains the construction of algebraic closure for countable fields (previously in countalg)
- proof of quantifier elimination for closed field rewritten in a monadic style
|
|
they are already defined in ssrfun
ChangeLog updated
|
|
[opam]: add dev-repo links
|
|
|
|
This commit fixes the following issue:
```shell
$ opam pin add coq-mathcomp-ssreflect --dev
[ERROR] "dev-repo" field missing in coq-mathcomp-ssreflect metadata,
you'll need to specify the pinning location
```
This commit also changes http to https for the homepage links.
|
|
Added the definition of all2.
This definition of all2 has the useful computational behaviour, and all2E unfolds an equivalent one.
|
|
Tool to prove only P0 -> P1 -> ... -> Pn -> P0
but use any implication Pi -> Pj
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
- Cleanup, refactoring and generalize the makefile architecture
- Reuses @strub math-comp/analysis Makefile / Makefile.common organization
- As #174, this fixes #88, but looks more stable than trying to fix the use of the MAKEFLAGS internal variable
|
|
Proofs by Cyril Cohen
|
|
small generalizations and extensions in poly
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
I had put this for compatibility with mathcomp 1.6 when we were still using svn, but I am afraid it got under the radar.
We should decide
- if we revert the change of `ltngtP`,
- if we document (and extend) the compatibility module
- or if we just remove the module and keep the change to `ltngtP`
I am personally in favour of the last
|
|
|
|
Dear devs, in an attempt to simplify the code of intro patterns we came up with a proposal that:
- simplifies the code of the plugin
- breaks only one line in the entire mathcomp, the one fixed by this patch.
The code we want to simplify is the one deferring clear switches inside an intro pattern.
The implementation is tricky because just delaying the clear switch until the end of the pattern is not enough, for example:
```
move=> {x} /andP[x y].
```
In this case `x` is both cleared and used. In order to be able to use `x`, given that the clear has not been performed yet, we rename `x` into `_x_` (when `{x}` is executed) so that when `x` is later executed we can use the name `x`, and then `.` is executed clear `_x_` instead of `x`.
So systematically "always rename now & clear later" seem to be OK, but it is not. The extra complication is that "rename" may break later intro pattern using terms as views. Eg
```
move=> {x} /andP[Ha Hb] /x.
```
What the code does today is:
- when `{x}` is execute look-ahead in the patter and see if `x` is used as a name to be introduced
- if so, "rename"
- otherwise don't rename (just delay)
This way of doing things is not only complicated but also incomplete, Eg
```
move=> {x} /orP[x | /x].
```
would misbehave, since the look-ahead is not "semantic".
Anyway, the proposed behavior is:
- `{x}` always renames now and clears (the renamed) later
- `{clears}/views` is always "compiled" as `/views{clears}` (most of the occurrences in the library are ok with this simpler rule, but for the one fixed in this PR).
- bonus: support `{}/view` (as in `rewrite {}rule`) to signal that the immediately following `view` has to be cleared, that is `{}/v` compiled as `/v{v}`.
What do you think?
```
```
|
