index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
/
ZArith
Mode
Name
Size
-rw-r--r--
BinInt.v
46012
log
plain
-rw-r--r--
BinIntDef.v
14793
log
plain
-rw-r--r--
Int.v
13491
log
plain
-rw-r--r--
Wf_Z.v
6000
log
plain
-rw-r--r--
ZArith.v
882
log
plain
-rw-r--r--
ZArith_base.v
1302
log
plain
-rw-r--r--
ZArith_dec.v
5354
log
plain
-rw-r--r--
Zabs.v
3572
log
plain
-rw-r--r--
Zbool.v
4876
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
21265
log
plain
-rw-r--r--
Zdiv_def.v
1718
log
plain
-rw-r--r--
Zeuclid.v
1747
log
plain
-rw-r--r--
Zeven.v
7915
log
plain
-rw-r--r--
Zgcd_alt.v
9688
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
1067
log
plain
-rw-r--r--
Znat.v
23028
log
plain
-rw-r--r--
Znumtheory.v
27906
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
16479
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
2397
log
plain
-rwxr-xr-x
intro.tex
238
log
plain
-rw-r--r--
vo.itarget
397
log
plain