Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison cardinal.agda @ 424:cc7909f86841

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
remvoe TransFinifte1
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 01 Aug 2020 23:37:10 +0900
parents 44a484f17f26
children f7d66c84bc26
comparison
equal deleted inserted replaced
423:9984cdd88da3 424:cc7909f86841
18 open inOrdinal O 18 open inOrdinal O
19 open OD O 19 open OD O
20 open OD.OD 20 open OD.OD
21 open OPair O 21 open OPair O
22 open ODAxiom odAxiom 22 open ODAxiom odAxiom
23
24 import OrdUtil
25 import ODUtil
26 open Ordinals.Ordinals O
27 open Ordinals.IsOrdinals isOrdinal
28 open Ordinals.IsNext isNext
29 open OrdUtil O
30 open ODUtil O
31
23 32
24 open _∧_ 33 open _∧_
25 open _∨_ 34 open _∨_
26 open Bool 35 open Bool
27 open _==_ 36 open _==_