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

diff src/generic-filter.agda @ 1218:362e43a1477c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
brain damaged fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 06 Mar 2023 10:45:34 +0900
parents 42000f20fdbe
children 5223f0b40d91
line wrap: on
line diff
--- a/src/generic-filter.agda	Sun Mar 05 23:49:10 2023 +0900
+++ b/src/generic-filter.agda	Mon Mar 06 10:45:34 2023 +0900
@@ -52,8 +52,7 @@
 open import Data.List hiding (filter)
 open import Data.Maybe 
 
-import OPair
-open OPair O
+open import ZProduct O
 
 record CountableModel : Set (suc (suc n)) where
    field