Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/logic.agda @ 326:a3fb231feeb9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
omega
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 21 Jan 2022 10:45:42 +0900
parents e5cf49902db3
children ba0ae5de62d1
comparison
equal deleted inserted replaced
325:39f0e1d7a7e5 326:a3fb231feeb9
71 true <=> true = true 71 true <=> true = true
72 false <=> false = true 72 false <=> false = true
73 _ <=> _ = false 73 _ <=> _ = false
74 74
75 open import Relation.Binary.PropositionalEquality 75 open import Relation.Binary.PropositionalEquality
76
77 not-not-bool : { b : Bool } → not (not b) ≡ b
78 not-not-bool {true} = refl
79 not-not-bool {false} = refl
76 80
77 record Bijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m) where 81 record Bijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m) where
78 field 82 field
79 fun← : S → R 83 fun← : S → R
80 fun→ : R → S 84 fun→ : R → S