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

comparison partfunc.agda @ 392:55f44ec2a0c6

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 Sat, 25 Jul 2020 17:36:27 +0900
parents 19687f3304c9
children 9984cdd88da3
comparison
equal deleted inserted replaced
391:e98b5774d180 392:55f44ec2a0c6
6 module partfunc {n : Level } (O : Ordinals {n}) where 6 module partfunc {n : Level } (O : Ordinals {n}) where
7 7
8 open import logic 8 open import logic
9 open import Relation.Binary 9 open import Relation.Binary
10 open import Data.Empty 10 open import Data.Empty
11 open import Data.List 11 open import Data.List hiding (filter)
12 open import Data.Maybe 12 open import Data.Maybe
13 open import Relation.Binary 13 open import Relation.Binary
14 open import Relation.Binary.Core 14 open import Relation.Binary.Core
15 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) 15 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
16 open import filter O 16 open import filter O