ZArith « theories - coq - the Coq proof assistant

Mode	Name	Size
-rw-r--r--	BinInt.v	51943	log plain
-rw-r--r--	BinIntDef.v	14879	log plain
-rw-r--r--	Int.v	13433	log plain
-rw-r--r--	Wf_Z.v	6003	log plain
-rw-r--r--	ZArith.v	841	log plain
-rw-r--r--	ZArith_base.v	1302	log plain
-rw-r--r--	ZArith_dec.v	4817	log plain
-rw-r--r--	Zabs.v	3577	log plain
-rw-r--r--	Zbool.v	4876	log plain
-rw-r--r--	Zcompare.v	5519	log plain
-rw-r--r--	Zcomplements.v	4792	log plain
-rw-r--r--	Zdigits.v	8966	log plain
-rw-r--r--	Zdiv.v	21332	log plain
-rw-r--r--	Zeuclid.v	1734	log plain
-rw-r--r--	Zeven.v	7871	log plain
-rw-r--r--	Zgcd_alt.v	9185	log plain
-rw-r--r--	Zhints.v	3916	log plain
-rw-r--r--	Zlogarithm.v	8614	log plain
-rw-r--r--	Zmax.v	2448	log plain
-rw-r--r--	Zmin.v	2218	log plain
-rw-r--r--	Zminmax.v	1151	log plain
-rw-r--r--	Zmisc.v	1077	log plain
-rw-r--r--	Znat.v	27576	log plain
-rw-r--r--	Znumtheory.v	26722	log plain
-rw-r--r--	Zorder.v	15215	log plain
-rw-r--r--	Zpow_alt.v	2561	log plain
-rw-r--r--	Zpow_def.v	1332	log plain
-rw-r--r--	Zpow_facts.v	8056	log plain
-rw-r--r--	Zpower.v	9555	log plain
-rw-r--r--	Zquot.v	14360	log plain
-rw-r--r--	Zsqrt_compat.v	7686	log plain
-rw-r--r--	Zwf.v	2542	log plain
-rw-r--r--	auxiliary.v	2397	log plain
-rwxr-xr-x	intro.tex	238	log plain
-rw-r--r--	vo.itarget	358	log plain