coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-02-19	Terminate some lemmas with Qed.	Guillaume Melquiond
	Since the proofs start by applying or destructuring Qed-ed lemmas, they cannot be used in a computational setting, so no need for them to be Defined.
2020-05-16	Prove that classical reals implement constructive reals. Also move sums, min ↵	Vincent Semeria
	and max to CoRN. Update stdlib index Remove ConstructiveSum from the index Add changelog entry Make constructive reals experimental
2020-05-09	Define CRzero and CRone via CR_of_Q	Vincent Semeria
	Add real numbers up to 10
2020-03-27	Cleanup stdlib reals. Use implicit arguments for ConstructiveReals. Move ↵	Vincent Semeria
	ConstructiveReals into new directory Abstract. Remove imports of implementations inside those Abstract files. Add changelog for constructive reals cleanup Move Cauchy reals into new directory Cauchy Update stdlib index Rename sum_f_R0 Use coqdoc comments Update doc/changelog/10-standard-library/11725-cleanup-reals.rst Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com> Update doc/changelog/10-standard-library/11725-cleanup-reals.rst Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com> Update doc/changelog/10-standard-library/11725-cleanup-reals.rst Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com> Improve notations