Kazuhiko Sakaguchi comments

Results 306 comments of


                                            Kazuhiko Sakaguchi

Revise use of numerical occurrence selectors

I wish to write patterns before `->` and ` [in RHS]

Revise use of numerical occurrence selectors

Enrico's remark: `move=> [in RHS]

Revise use of numerical occurrence selectors

> In order to process the other directories as a collective effort, > could you share the small tools (sed, perl scripts, patterns to be grepped, etc.) > or ideas...

[meta-issue] Clanup using features of Arguments

Probably a related question: why the `%|` notation in `intdiv` is defined in this way using `\in`? Is this only because of simulating `simpl never`? https://github.com/math-comp/math-comp/blob/3515b33b1245ea169fbaf61405dc60954509fee2/mathcomp/algebra/intdiv.v#L70

Modular lattice of linear subspaces

These lattices also seem to be complemented and graded but non-distributive. There might be so many missing structures.

Modular lattice of linear subspaces

Since the complement of linear subspaces is not unique, I am not sure whether we should have such complemented non-distributive lattice structures anymore. Declaring the canonical `tbLatticeType` of them and...

Removing `dffun` in favor of `ffun`?

IIUC, the limitation still exists and coq/coq#12349 removes it.

Removing `dffun` in favor of `ffun`?

Also, this issue is a part of #606.

Removing `dffun` in favor of `ffun`?

> IIUC, the limitation still exists and [coq/coq#12349](https://github.com/coq/coq/pull/12349) removes it. This was not true. The limitation still exists but is a different one. If I generalize `{ffun fT}` to subsume...

Use predicators even extensively

@CohenCyril I agree. This PR also breaks odd-order by changing argument scopes of some lemmas, but putting all the scope information back by `Arguments` command seems too much to do.