Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison 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 |
comparison
equal
deleted
inserted
replaced
227:a4cdfc84f65f | 228:49736efc822b |
---|---|
481 Union = ZF.Union OD→ZF | 481 Union = ZF.Union OD→ZF |
482 Power = ZF.Power OD→ZF | 482 Power = ZF.Power OD→ZF |
483 Select = ZF.Select OD→ZF | 483 Select = ZF.Select OD→ZF |
484 Replace = ZF.Replace OD→ZF | 484 Replace = ZF.Replace OD→ZF |
485 isZF = ZF.isZF OD→ZF | 485 isZF = ZF.isZF OD→ZF |
486 TransFinite = IsOrdinals.TransFinite (Ordinals.isOrdinal O) |