coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
\| *	GRAMMAR: added punctuation	Matej Kosik	2015-12-10
\| \|
\| *	CLEANUP PROPOSITION: rephrasing the original idea in a simpler way	Matej Kosik	2015-12-10
\| \|
\| *	CLEANUP PROPOSITION: existing example was removed because it is not urgently ↵	Matej Kosik	2015-12-10
\| \| \| \| \| \| \| \|	needed
\| *	ENH: existing example was changed so that it is now linked to the results ↵	Matej Kosik	2015-12-10
\| \| \| \| \| \| \| \|	shown in the previous example
\| *	ENH: an existing example was further expanded.	Matej Kosik	2015-12-10
\| \|
\| *	CLEANUP: Existing example was removed.	Matej Kosik	2015-12-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	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.
\| *	ENH: existing example was expanded	Matej Kosik	2015-12-10
\| \|
\| *	ENH: define the meaning of 'p'	Matej Kosik	2015-12-10
\| \|
\| *	CLEANUP PROPOSITION: does it make sense to refer to 'I' as 'inductive ↵	Matej Kosik	2015-12-10
\| \| \| \| \| \| \| \|	definition'? Doesn't make more sense to refer to it as 'inductive type'?
\| *	CLEANUP: We decided to call these guys E[Γ] ⊢ (Γi := Γc) as inductive ↵	Matej Kosik	2015-12-10
\| \| \| \| \| \| \| \|	definition.
\| *	COMMENT: question	Matej Kosik	2015-12-10
\| \|
\| *	CLEANUP: removing a superfluous index	Matej Kosik	2015-12-10
\| \|
\| *	COMMENT: question	Matej Kosik	2015-12-10
\| \|
\| *	COMMENT: question	Matej Kosik	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	2015-12-10
\| \| \| \| \| \| \| \|	elimination sorts" is actually used
\| *	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
\| \|