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

diff ordinal.agda @ 97:f2b579106770

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
power set using sup on Def
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 09 Jun 2019 19:41:53 +0900
parents 4659a815b70d
children 1daa1d24348c
line wrap: on
line diff
--- a/ordinal.agda	Sat Jun 08 22:17:40 2019 +0900
+++ b/ordinal.agda	Sun Jun 09 19:41:53 2019 +0900
@@ -289,3 +289,4 @@
 TransFinite caseΦ caseOSuc record { lv = lv ; ord = (Φ (lv)) } = caseΦ lv
 TransFinite caseΦ caseOSuc record { lv = lx ; ord = (OSuc lx ox) } = 
       caseOSuc lx ox (TransFinite caseΦ caseOSuc  record { lv = lx ; ord = ox })
+