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

changeset 1253:507f443c97ce

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 Wed, 15 Mar 2023 22:45:05 +0900
parents c99c37121d47
children abd86d493c61
files src/generic-filter.agda
diffstat 1 files changed, 1 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/src/generic-filter.agda	Wed Mar 15 22:26:00 2023 +0900
+++ b/src/generic-filter.agda	Wed Mar 15 22:45:05 2023 +0900
@@ -451,18 +451,10 @@
     M∋DM = is-model C D ?
     D⊆PP : D ⊆ Power P
     D⊆PP {x} ⟪ Lx , ngx ⟫  = LPP Lx 
-    -- ll01 : {q r : HOD } → (rgf ∋ q) ∧ (rgf ∋ r) → (q ⊆ (q ∪ r) ) ∧ (r ⊆ (q ∪ r) )
-    -- ll01 {q} {r} rgfpq with  gfilter2 PG rgfpq 
-    -- ... | record { z = z₁ ; az = record { z = z ; az = az ; x=ψz = x=ψz₁ } ; x=ψz = x=ψz } = ?
-    --   ll02 : {x : Ordinal } → odef q x → odef rgf x
-    --    ll02 {x} qx = record { z = ? ; az = record { z = ? ; az = ? ; x=ψz = ? }  ; x=ψz = ? }
-    --    -- filter2 GF ? ? ?
-    -- with contra-position ? ?
-    -- ... | t = ?
     DD : Dense {L} {P} LPP
     Dense.dense DD = D
     Dense.d⊆P DD ⟪ Lx , _ ⟫ = Lx
-    Dense.dense-f DD Lp = ? where
+    Dense.dense-f DD Lp = ll00 where
         ll00 : HOD
         ll00 with NotCompatible.¬compat (NC Lp)
         ... | nc = ?