Mercurial > hg > Members > kono > Proof > ZF-in-agda
directory /src/ @ 1485:5dacb669f13b
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 | 44180 | -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-- |