Kazuhiko Sakaguchi

Fix issues related to listings

5

This PR introduces a new class option `listing=(listings|minted)` and fixes #236. Now, `kao.sty` requires either `listings.sty` or `minted.sty` depending on the users' choice. The `marginlisting` environment supports only the chosen...

### Description I experienced several issues related to listings, such as: - the wide listing (`listing*`) environment is not available (should eventually be fixed in #225), - the caption and...

Currently, hyphens are printed before and after each margin figure, table, or listing. Writing an expression to calculate length as the argument of \vspace requires \dimexpr.

Print "nodate" in \sidecite if year is unspecified

1

Before this change, by using `\sidecite` for an entry where `year` is unspecified, I get: > [1]: Author (), Title and with this change, I get: > [1]: Author (n.d.),...

Modular lattice of linear subspaces

4

The subspaces `{vspace vT}` of a vector space `vT` (defined in `vector.v`) seem to form a lattice. [A Wikipedia article](https://en.wikipedia.org/wiki/Linear_subspace) says that "the operations intersection and sum make the set...

[DO NOT MERGE] Attempt to remove dffun

3

##### Motivation for this change This PR attempts to merge `{dffun fT}` and `{ffun fT}` to close issue #701, but it is unsuccessful due to some limitations of unification. I...

[WIP] Make linear subspaces canonically a `tbLatticeType`

2

##### Motivation for this change This is my first attempt to make linear subspaces `{vspace vT}` canonically a `tbLatticeType`. In `vector.v`, some operators for linear subspace (`subsetv`, `fullv`, `addv`, and...

Extending `rel` theory

3

Currently, support for the following items is lacking: - Union, intersection, complement, and converse of binary relations: > [...] Should we introduce some notation for relI, (e.g., `[relI e1 &...

Use predicators even extensively

4

##### Motivation for this change This PR attempts to restate several lemmas using predicators such as `cancel`, `(left|right)_(id|zero|inverse|distributive)`, `idempotent`, `associative`, and `commutative`. Some of them are probably too aggressive and...

`((_ %/ _) %/ _)%Z` does not typecheck if polydiv is imported

11

```coq From mathcomp Require Import all_ssreflect all_algebra. Fail Check ((_ %/ _) %/ _)%Z. ``` ``` The command has indeed failed with message: The term "(?p %/ ?q)%R" has type...