stdlib2
stdlib2 copied to clipboard
coq
@CohenCyril and I will extend https://github.com/math-comp/math-comp/blob/master/CONTRIBUTING.md#statements-of-lemmas-theorems-and-definitions These conventions will be used in stdlib2. Their description should be moved to the stdlib2 repository, and missing/unclear conventions can be discussed here.
I would like to mention an approach which has been useful in uniformizing the layout of files of the standard library and giving a feeling of homogeneity of style, which...
I wish all types (type families) in the standard library came with a distinguished notions of validity and equivalence, ideally expressed using a partial equivalence relations. For example `nat_per :=...
The prelude is the set of definitions / plugins loaded as soon as Coq starts. I would like to keep it minimal. I imagine we would like to get at...