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

comparison OPair.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
5 module OPair {n : Level } (O : Ordinals {n}) where 5 module OPair {n : Level } (O : Ordinals {n}) where
6 6
7 open import zf 7 open import zf
8 open import logic 8 open import logic
9 import OD 9 import OD
10 import ODUtil
11 import OrdUtil
10 12
11 open import Relation.Nullary 13 open import Relation.Nullary
12 open import Relation.Binary 14 open import Relation.Binary
13 open import Data.Empty 15 open import Data.Empty
14 open import Relation.Binary 16 open import Relation.Binary
19 open inOrdinal O 21 open inOrdinal O
20 open OD O 22 open OD O
21 open OD.OD 23 open OD.OD
22 open OD.HOD 24 open OD.HOD
23 open ODAxiom odAxiom 25 open ODAxiom odAxiom
26
27 open Ordinals.Ordinals O
28 open Ordinals.IsOrdinals isOrdinal
29 open Ordinals.IsNext isNext
30 open OrdUtil O
31 open ODUtil O
32
24 33
25 open _∧_ 34 open _∧_
26 open _∨_ 35 open _∨_
27 open Bool 36 open Bool
28 37