Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/libbijection.agda @ 405:af8f630b7e60

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, 24 Sep 2023 18:02:04 +0900
parents cd73fe566291
children
comparison
equal deleted inserted replaced
404:dfaf230f7b9a 405:af8f630b7e60
1 {-# OPTIONS --cubical-compatible --safe #-}
2
1 module libbijection where 3 module libbijection where
2 4
3 open import Level renaming ( zero to Zero ; suc to Suc ) 5 open import Level renaming ( zero to Zero ; suc to Suc )
4 open import Data.Nat 6 open import Data.Nat
5 open import Data.Maybe 7 open import Data.Maybe
6 open import Data.List hiding ([_] ; sum ) 8 open import Data.List hiding ([_] ; sum )
7 open import Data.Nat.Properties 9 open import Data.Nat.Properties
8 open import Relation.Nullary 10 open import Relation.Nullary
9 open import Data.Empty 11 open import Data.Empty
10 open import Data.Unit hiding ( _≤_ ) 12 open import Data.Unit
11 open import Relation.Binary.Core hiding (_⇔_) 13 open import Relation.Binary.Core hiding (_⇔_)
12 open import Relation.Binary.Definitions 14 open import Relation.Binary.Definitions
13 open import Relation.Binary.PropositionalEquality 15 open import Relation.Binary.PropositionalEquality
14 open import Function.Inverse hiding (sym) 16 open import Function.Inverse hiding (sym)
15 open import Function.Bijection renaming (Bijection to Bijection1) 17 open import Function.Bijection renaming (Bijection to Bijection1)