Quentin VERMANDE
Quentin VERMANDE
Strengthens convA' and convACA' and adds a few lemmas. Defines l-modules as convex spaces. Proves Carathéodory's Theorem. Contains general purpose lemmas that should not stay here (e.g. everything in section...
Draft for a modification of the unification algorithm, to see how much it breaks the CI. For now, it catches unification problems where one of the term is a projection...
Preorder
##### Motivation for this change Defines preordered types and generalizes lemmas on `porderType` to `preorderType`. ##### Things done/to do - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [x] added corresponding...
The mulr_closed predicate asks for the subset to contain 1, which is not the case for subalgebras ({aspace _} in field/falgebra.v). Yet these are closed under multiplication and I would...
##### Motivation for this change Part of the inference mechanism was missing and the canonical structures were not accessible. ##### Checklist - [ ] added corresponding entries in `CHANGELOG_UNRELEASED.md` -...
Wochoice
##### Motivation for this change Adds a proof of Zorn's lemma, Hausdorff maximal principle and the well ordering principle. Contains a patch of contra that we may want to extract....
It may happen that coq-elpi aliases something in the input evar_map and then drops the alias because it does not appear in the solution returned by coq-elpi. However, this alias...
Hi. It looks like it is not possible to add a clause to a predicate immediately after the creation of the predicate, as the following code shows. ``` From elpi.apps...
In the following script, I have an element `T` of some structure `S` and I try to coerce an element `x` of `T` into `@sig T P`. The coercion search...