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

changeset 1262:db274ca4c55c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 19 Mar 2023 12:21:10 +0900
parents 2fccbe475cf7
children d04fb4b2c72b
files src/generic-filter.agda
diffstat 1 files changed, 5 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/src/generic-filter.agda	Sat Mar 18 15:59:17 2023 +0900
+++ b/src/generic-filter.agda	Sun Mar 19 12:21:10 2023 +0900
@@ -368,3 +368,8 @@
   ind : (x : Ordinal) → ((y : Ordinal) → y o< x → HOD) → HOD
   ind x valy = record { od = record { def = λ y → valS x y (& (⊆-Ideal.ideal (genf G))) } ; odmax = {!!} ; <odmax = {!!} }
 
+
+
+
+
+