| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-12-10 | GRAMMAR | Matej Kosik | |
| 2015-12-10 | COMMENT: note | Matej Kosik | |
| 2015-12-10 | TYPOGRAPHY | Matej Kosik | |
| 2015-12-10 | CLEANUP: originally, we talked about "B" as an "arity" | Matej Kosik | |
| 2015-12-10 | COMMENT: question | Matej Kosik | |
| 2015-12-10 | ENH: a forward reference to a place where the concept of "allowed ↵ | Matej Kosik | |
| elimination sorts" is actually used | |||
| 2015-12-10 | COMMENT: question | Matej Kosik | |
| 2015-12-10 | CLEANUP: unnecessary | Matej Kosik | |
| 2015-12-10 | GRAMMAR | Matej Kosik | |
| 2015-12-10 | COMMENT: question | Matej Kosik | |
| 2015-12-10 | ENH: improving precision | Matej Kosik | |
| 2015-12-10 | COMMENT: question | Matej Kosik | |
| 2015-12-10 | FIX: "u_p" was not defined | Matej Kosik | |
| 2015-12-10 | CLEANUP: removing duplicate paragraph | Matej Kosik | |
| 2015-12-10 | COMMENT: question | Matej Kosik | |
| 2015-12-10 | COMMENT: question | Matej Kosik | |
| 2015-12-10 | COMMENT: questions and to do | Matej Kosik | |
| 2015-12-10 | FIX: removing references to Γ which is not defined in a given context | Matej Kosik | |
| 2015-12-10 | TYPESETTING | Matej Kosik | |
| 2015-12-10 | COMMENT: question | Matej Kosik | |
| 2015-12-10 | GRAMMAR | Matej Kosik | |
| 2015-12-10 | CLEANUP PROPOSITION: superfluous parentheses were removed | Matej Kosik | |
| 2015-12-10 | CLEANUP PROPOSITION: s/local context of parameters/context of parameters | Matej Kosik | |
| 2015-12-10 | COMMENT: question | Matej Kosik | |
| 2015-12-10 | COMMENT: question | Matej Kosik | |
| 2015-12-10 | COMMENT: questions | Matej Kosik | |
| 2015-12-10 | COMMENT: to do | Matej Kosik | |
| 2015-12-10 | COMMENT: to do | Matej Kosik | |
| 2015-12-10 | FIX: removing a reference to \Gamma, because it is undefined | Matej Kosik | |
| 2015-12-10 | COMMENT: question | Matej Kosik | |
| 2015-12-10 | FIX: making sure that my previous edits do not break HTML generation | Matej Kosik | |
| 2015-12-10 | COMMENT: questions | Matej Kosik | |
| 2015-12-10 | ENH: examples for 'strict positivity' were expanded | Matej Kosik | |
| 2015-12-10 | COMMENT: question | Matej Kosik | |
| 2015-12-10 | CLEANUP: s/List_A/List~A/g | Matej Kosik | |
| 2015-12-10 | COMMENT: question | Matej Kosik | |
| 2015-12-10 | CLEANUP: the definition of "type of constructor" was rephrased in order to ↵ | Matej Kosik | |
| make it more clear | |||
| 2015-12-10 | COMMENT: question | Matej Kosik | |
| 2015-12-10 | COMMENT: question | Matej Kosik | |
| 2015-12-10 | COMMENT: to do | Matej Kosik | |
| 2015-12-10 | FIX: commit 315f771 | Matej Kosik | |
| 2015-12-10 | CLEANUP: superfluous examples were removed | Matej Kosik | |
| 2015-12-10 | ENH: new example: "even" | Matej Kosik | |
| 2015-12-10 | ALPHA-CONVERSION: s/Length/has_length/g | Matej Kosik | |
| 2015-12-10 | ENH: examples | Matej Kosik | |
| 2015-12-10 | TYPOGRAPHY: Examples of "arity" concept(s) were put to a separate ↵ | Matej Kosik | |
| \paragraph{...} | |||
| 2015-12-10 | ENH: adding a definition of the concept "_ is an arity". | Matej Kosik | |
| There already exists a definition of the following concept: "_ is an arity of sort _" I was not 100% sure what the following concept (used later in the text) means: "_ is an arity" so I added this (simple) definition in order to avoid possible confusion. | |||
| 2015-12-10 | TYPOGRAPHY | Matej Kosik | |
| 2015-12-10 | TYPOGRAPHY | Matej Kosik | |
| 2015-12-10 | COMMENT: to do | Matej Kosik | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |