Mercurial > hg > Members > kono > Proof > ZF-in-agda
directory /src/ @ 1477:88fdc41868f9
name | size | permissions |
---|---|---|
[up] | drwxr-xr-x | |
BAlgebra.agda | 12701 | -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 | 30688 | -rw-r--r-- |
ODC.agda | 4481 | -rw-r--r-- |
ODUtil.agda | 12931 | -rw-r--r-- |
OrdUtil.agda | 11397 | -rw-r--r-- |
Ordinals.agda | 2086 | -rw-r--r-- |
PFOD.agda | 10071 | -rw-r--r-- |
README.md | 3694 | -rw-r--r-- |
Topology.agda | 42699 | -rw-r--r-- |
Tychonoff.agda | 30878 | -rw-r--r-- |
VL.agda | 2115 | -rw-r--r-- |
ZProduct.agda | 42936 | -rw-r--r-- |
bijection.agda | 54214 | -rw-r--r-- |
cardinal.agda | 27454 | -rw-r--r-- |
filter-util.agda | 23400 | -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 | 10452 | -rw-r--r-- |
nat.agda | 34032 | -rw-r--r-- |
ordinal.agda | 12444 | -rw-r--r-- |
partfunc.agda | 12206 | -rw-r--r-- |
zf.agda | 4884 | -rw-r--r-- |
zfc.agda | 886 | -rw-r--r-- |
zorn.agda | 101531 | -rw-r--r-- |