Mercurial > hg > Members > Moririn

comparison logic.agda @ 609:79418701a283

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add test and speciication
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 04 Nov 2021 16:35:11 +0900
parents 2075785a124a
children 0b791ae19543
comparison
equal deleted inserted replaced
608:8df36383ced0 609:79418701a283
12 data Bool : Set where 12 data Bool : Set where
13 true : Bool 13 true : Bool
14 false : Bool 14 false : Bool
15 15
16 record _∧_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where 16 record _∧_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where
17 constructor ⟪_,_⟫
17 field 18 field
18 proj1 : A 19 proj1 : A
19 proj2 : B 20 proj2 : B
20 21
21 data _∨_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where 22 data _∨_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where