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
33995
log
plain
-rw-r--r--
Int.v
13483
log
plain
-rw-r--r--
Wf_Z.v
8190
log
plain
-rw-r--r--
ZArith.v
878
log
plain
-rw-r--r--
ZArith_base.v
1269
log
plain
-rw-r--r--
ZArith_dec.v
5472
log
plain
-rw-r--r--
Zabs.v
6473
log
plain
-rw-r--r--
Zbool.v
6790
log
plain
-rw-r--r--
Zcompare.v
20230
log
plain
-rw-r--r--
Zcomplements.v
6040
log
plain
-rw-r--r--
Zdigits.v
9116
log
plain
-rw-r--r--
Zdiv.v
20871
log
plain
-rw-r--r--
Zdiv_def.v
10556
log
plain
-rw-r--r--
Zeuclid.v
1755
log
plain
-rw-r--r--
Zeven.v
10334
log
plain
-rw-r--r--
Zgcd_alt.v
9713
log
plain
-rw-r--r--
Zgcd_def.v
4493
log
plain
-rw-r--r--
Zhints.v
14072
log
plain
-rw-r--r--
Zlog_def.v
1914
log
plain
-rw-r--r--
Zlogarithm.v
8265
log
plain
-rw-r--r--
Zmax.v
3636
log
plain
-rw-r--r--
Zmin.v
3076
log
plain
-rw-r--r--
Zminmax.v
1183
log
plain
-rw-r--r--
Zmisc.v
3070
log
plain
-rw-r--r--
Znat.v
7521
log
plain
-rw-r--r--
Znumtheory.v
32803
log
plain
-rw-r--r--
Zorder.v
30337
log
plain
-rw-r--r--
Zpow_def.v
3537
log
plain
-rw-r--r--
Zpow_facts.v
15054
log
plain
-rw-r--r--
Zpower.v
9960
log
plain
-rw-r--r--
Zquot.v
15563
log
plain
-rw-r--r--
Zsqrt_compat.v
7786
log
plain
-rw-r--r--
Zsqrt_def.v
1679
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
382
log
plain