Cyril Cohen issues

Results 143 issues of


                                            Cyril Cohen

Have notations for deriving and derivability

Provide and document derivation notations such as: - ``f^`(n)``, ``f^`()`` and ``f^`N(n)`` (as in `poly.v`) for derivation on`R` (and when available, on `C`) - `'D(A -> V)` for the type...

enhancement :sparkles:

question :question:

documentation :memo:

renaming/refactoring :wrench:

Shouldn't a normed module be of dimension at least 1?

Indeed, otherwise locally' is not proper. Other issues? One way or another?

kind: question

kind: experiment

Have comap : A -> B -> set (set B) -> set (set A)

And define weak and sup filteredType, compare with weak and sup topology. And define the prod as the sup of the two comaps of π₁ and π₂. Credit @johoelzl for...

experiment :test_tube:

renaming/refactoring

Replace Filter by pfilter_on

Try to substitute canonical structures for typeclasses everywhere, so that we only use CS instead of TC... (And maybe put in filteredType the axiom that canonical sets of sets must...

experiment :test_tube:

renaming/refactoring

changing def of ratio, and renamings

- ratio v w now defaults to 0 when v is not proptional to w - contraction and extension renaming to scaling - refactored proof of scaling_bet - introduced fun...

Name clash in printing of results of derive.param2

```coq From elpi Require Import derive. Elpi derive.param2 eq. Print eq_R. ``` prints ```coq Inductive eq_R (A A : Type) (A : A -> A -> Type) (x x :...

Adding NES.Export

NES.Snapshot takes a "picture" of the current state of a Namespace, for later reuse without the namespace commands.

@clarus I just realized that this package was added and committed in https://github.com/coq/opam-coq-archive/commit/51d43887e025dd7e4da545e4872e135d5b9a769b with maintainer "Mathematical Components ". To my knowledge this has not been discussed there, and this package...

Cyril Cohen