Mercurial > hg > Members > kono > Proof > automaton1

comparison Test.agda @ 0:9615a94b18ca

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
new automaton in agda
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 12 Nov 2020 11:45:34 +0900
parents
children
comparison
equal deleted inserted replaced
-1:000000000000 0:9615a94b18ca
1 module Test where
2 open import Level
3 open import Relation.Nullary
4 open import Relation.Binary -- hiding (_⇔_ )
5 open import Data.Empty
6 open import Data.Nat hiding ( _⊔_ )
7
8 id : ( A : Set ) → A → A
9 id A x = x
10
11 id1 : { A : Set } → A → A
12 id1 x = x
13
14
15 test1 = id ℕ 1
16 test2 = id1 1
17
18
19
20 data Bool : Set where
21 true : Bool
22 false : Bool
23
24 record _∧_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where
25 constructor ⟪_,_⟫
26 field
27 proj1 : A
28 proj2 : B
29
30 data _∨_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where
31 case1 : A → A ∨ B
32 case2 : B → A ∨ B