Mercurial > hg > Members > kono > Proof > ZF-in-agda
directory /src/ @ 1486:49c3ef1e9b4f
| name | size | permissions |
|---|---|---|
| [up] | drwxr-xr-x | |
 BAlgebra.agda
|
13005 | -rw-r--r-- |
|
HODBase.agda
|
3730 | -rw-r--r-- |
|
LEMC.agda
|
7591 | -rw-r--r-- |
|
LICENSE
|
35149 | -rw-r--r-- |
|
NSet.agda
|
2284 | -rw-r--r-- |
|
OD.agda
|
30764 | -rw-r--r-- |
|
ODC.agda
|
4481 | -rw-r--r-- |
|
ODUtil.agda
|
13811 | -rw-r--r-- |
|
OrdUtil.agda
|
11397 | -rw-r--r-- |
|
Ordinals.agda
|
2083 | -rw-r--r-- |
|
PFOD.agda
|
10071 | -rw-r--r-- |
|
README.md
|
3694 | -rw-r--r-- |
|
Topology.agda
|
43947 | -rw-r--r-- |
|
Tychonoff.agda
|
30878 | -rw-r--r-- |
|
VL.agda
|
2115 | -rw-r--r-- |
|
ZProduct.agda
|
43564 | -rw-r--r-- |
|
bijection.agda
|
54214 | -rw-r--r-- |
|
cardinal.agda
|
27454 | -rw-r--r-- |
|
filter-util.agda
|
24917 | -rw-r--r-- |
|
filter.agda
|
16230 | -rw-r--r-- |
|
generic-filter.agda
|
16758 | -rw-r--r-- |
|
logic.agda
|
5266 | -rw-r--r-- |
|
maximum-filter.agda
|
10527 | -rw-r--r-- |
|
nat.agda
|
34032 | -rw-r--r-- |
|
ordinal.agda
|
12471 | -rw-r--r-- |
|
partfunc.agda
|
12206 | -rw-r--r-- |
|
zf.agda
|
4884 | -rw-r--r-- |
|
zfc.agda
|
886 | -rw-r--r-- |
|
zorn.agda
|
98577 | -rw-r--r-- |