aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2015-12-10COMMENT: questionMatej Kosik
2015-12-10COMMENT: to doMatej Kosik
2015-12-10GRAMMAR: added punctuationMatej Kosik
2015-12-10CLEANUP PROPOSITION: rephrasing the original idea in a simpler wayMatej Kosik
2015-12-10CLEANUP PROPOSITION: existing example was removed because it is not urgently ↵Matej Kosik
needed
2015-12-10ENH: existing example was changed so that it is now linked to the results ↵Matej Kosik
shown in the previous example
2015-12-10ENH: an existing example was further expanded.Matej Kosik
2015-12-10CLEANUP: Existing example was removed.Matej Kosik
We have expanded the example above. For consistency reasons, it would make sense to do the same also for this example. However, due to the size of the terms, it is hard to typeset it nicely. I propose to remove it.
2015-12-10ENH: existing example was expandedMatej Kosik
2015-12-10ENH: define the meaning of 'p'Matej Kosik
2015-12-10CLEANUP PROPOSITION: does it make sense to refer to 'I' as 'inductive ↵Matej Kosik
definition'? Doesn't make more sense to refer to it as 'inductive type'?
2015-12-10CLEANUP: We decided to call these guys E[Γ] ⊢ (Γi := Γc) as inductive ↵Matej Kosik
definition.
2015-12-10COMMENT: questionMatej Kosik
2015-12-10CLEANUP: removing a superfluous indexMatej Kosik
2015-12-10COMMENT: questionMatej Kosik
2015-12-10COMMENT: questionMatej Kosik
2015-12-10GRAMMARMatej Kosik
2015-12-10COMMENT: noteMatej Kosik
2015-12-10TYPOGRAPHYMatej Kosik
2015-12-10CLEANUP: originally, we talked about "B" as an "arity"Matej Kosik
2015-12-10COMMENT: questionMatej Kosik
2015-12-10ENH: a forward reference to a place where the concept of "allowed ↵Matej Kosik
elimination sorts" is actually used
2015-12-10COMMENT: questionMatej Kosik
2015-12-10CLEANUP: unnecessaryMatej Kosik
2015-12-10GRAMMARMatej Kosik
2015-12-10COMMENT: questionMatej Kosik
2015-12-10ENH: improving precisionMatej Kosik
2015-12-10COMMENT: questionMatej Kosik
2015-12-10FIX: "u_p" was not definedMatej Kosik
2015-12-10CLEANUP: removing duplicate paragraphMatej Kosik
2015-12-10COMMENT: questionMatej Kosik
2015-12-10COMMENT: questionMatej Kosik
2015-12-10COMMENT: questions and to doMatej Kosik
2015-12-10FIX: removing references to Γ which is not defined in a given contextMatej Kosik
2015-12-10TYPESETTINGMatej Kosik
2015-12-10COMMENT: questionMatej Kosik
2015-12-10GRAMMARMatej Kosik
2015-12-10CLEANUP PROPOSITION: superfluous parentheses were removedMatej Kosik
2015-12-10CLEANUP PROPOSITION: s/local context of parameters/context of parametersMatej Kosik
2015-12-10COMMENT: questionMatej Kosik
2015-12-10COMMENT: questionMatej Kosik
2015-12-10COMMENT: questionsMatej Kosik
2015-12-10COMMENT: to doMatej Kosik
2015-12-10COMMENT: to doMatej Kosik
2015-12-10FIX: removing a reference to \Gamma, because it is undefinedMatej Kosik
2015-12-10COMMENT: questionMatej Kosik
2015-12-10FIX: making sure that my previous edits do not break HTML generationMatej Kosik
2015-12-10COMMENT: questionsMatej Kosik
2015-12-10ENH: examples for 'strict positivity' were expandedMatej Kosik
2015-12-10COMMENT: questionMatej Kosik
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 10:51:25 +0000