diff OD.agda @ 228:49736efc822b

try transfinite
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 11 Aug 2019 20:42:48 +0900
parents 176ff97547b4
children e06b76e5b682
line wrap: on
line diff
--- a/OD.agda	Sun Aug 11 18:37:33 2019 +0900
+++ b/OD.agda	Sun Aug 11 20:42:48 2019 +0900
@@ -483,3 +483,4 @@
 Select = ZF.Select OD→ZF
 Replace = ZF.Replace OD→ZF
 isZF = ZF.isZF  OD→ZF
+TransFinite = IsOrdinals.TransFinite (Ordinals.isOrdinal O)