Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison generic-filter.agda @ 424:cc7909f86841
remvoe TransFinifte1
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 01 Aug 2020 23:37:10 +0900 |
parents | 44a484f17f26 |
children | 9b0630f03c4b |
comparison
equal
deleted
inserted
replaced
423:9984cdd88da3 | 424:cc7909f86841 |
---|---|
21 | 21 |
22 open inOrdinal O | 22 open inOrdinal O |
23 open OD O | 23 open OD O |
24 open OD.OD | 24 open OD.OD |
25 open ODAxiom odAxiom | 25 open ODAxiom odAxiom |
26 import OrdUtil | |
27 import ODUtil | |
28 open Ordinals.Ordinals O | |
29 open Ordinals.IsOrdinals isOrdinal | |
30 open Ordinals.IsNext isNext | |
31 open OrdUtil O | |
32 open ODUtil O | |
33 | |
26 | 34 |
27 import ODC | 35 import ODC |
28 | 36 |
29 open filter O | 37 open filter O |
30 | 38 |