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

diff OD.agda @ 235:846e0926bb89

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix cardinal
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 15 Aug 2019 04:51:24 +0900
parents e06b76e5b682
children d09437fcfc7c
line wrap: on
line diff
--- a/OD.agda	Tue Aug 13 22:21:10 2019 +0900
+++ b/OD.agda	Thu Aug 15 04:51:24 2019 +0900
@@ -490,7 +490,7 @@
                  ψ : ( ox : Ordinal ) → Set (suc n)
                  ψ ox = (( x : Ordinal ) → x o< ox  → ( ¬ def X x )) ∨ choiced X
                  lemma-ord : ( ox : Ordinal  ) → ψ ox
-                 lemma-ord  ox = IsOrdinals.TransFinite (Ordinals.isOrdinal O) {ψ} induction ox where
+                 lemma-ord  ox = TransFinite {ψ} induction ox where
                     ∋-p : (A x : OD ) → Dec ( A ∋ x ) 
                     ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x ))
                     ∋-p A x | case1 (lift t)  = yes t
@@ -530,4 +530,3 @@
 Select = ZF.Select OD→ZF
 Replace = ZF.Replace OD→ZF
 isZF = ZF.isZF  OD→ZF
-TransFinite = IsOrdinals.TransFinite (Ordinals.isOrdinal O)