ZArith « theories - coq - the Coq proof assistant

Mode	Name	Size
-rw-r--r--	BinInt.v	45950	log plain
-rw-r--r--	BinIntDef.v	14793	log plain
-rw-r--r--	Int.v	13491	log plain
-rw-r--r--	Wf_Z.v	8136	log plain
-rw-r--r--	ZArith.v	891	log plain
-rw-r--r--	ZArith_base.v	1293	log plain
-rw-r--r--	ZArith_dec.v	5354	log plain
-rw-r--r--	Zabs.v	5414	log plain
-rw-r--r--	Zbool.v	6567	log plain
-rw-r--r--	Zcompare.v	5518	log plain
-rw-r--r--	Zcomplements.v	6040	log plain
-rw-r--r--	Zdigits.v	9105	log plain
-rw-r--r--	Zdigits_def.v	10744	log plain
-rw-r--r--	Zdiv.v	21246	log plain
-rw-r--r--	Zdiv_def.v	1718	log plain
-rw-r--r--	Zeuclid.v	1747	log plain
-rw-r--r--	Zeven.v	9269	log plain
-rw-r--r--	Zgcd_alt.v	9713	log plain
-rw-r--r--	Zgcd_def.v	1061	log plain
-rw-r--r--	Zhints.v	14072	log plain
-rw-r--r--	Zlog_def.v	713	log plain
-rw-r--r--	Zlogarithm.v	8628	log plain
-rw-r--r--	Zmax.v	3372	log plain
-rw-r--r--	Zmin.v	2899	log plain
-rw-r--r--	Zminmax.v	1151	log plain
-rw-r--r--	Zmisc.v	1065	log plain
-rw-r--r--	Znat.v	21812	log plain
-rw-r--r--	Znumtheory.v	32803	log plain
-rw-r--r--	Zorder.v	15061	log plain
-rw-r--r--	Zpow_def.v	3786	log plain
-rw-r--r--	Zpow_facts.v	15103	log plain
-rw-r--r--	Zpower.v	9928	log plain
-rw-r--r--	Zquot.v	16459	log plain
-rw-r--r--	Zsqrt_compat.v	7768	log plain
-rw-r--r--	Zsqrt_def.v	911	log plain
-rw-r--r--	Zwf.v	2644	log plain
-rw-r--r--	auxiliary.v	3515	log plain
-rwxr-xr-x	intro.tex	238	log plain
-rw-r--r--	vo.itarget	409	log plain