Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison logic.agda @ 387:8b0715e28b33
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 25 Jul 2020 09:09:00 +0900 |
parents | 22d435172d1a |
children | 44a484f17f26 |
comparison
equal
deleted
inserted
replaced
386:24a66a246316 | 387:8b0715e28b33 |
---|---|
3 open import Level | 3 open import Level |
4 open import Relation.Nullary | 4 open import Relation.Nullary |
5 open import Relation.Binary | 5 open import Relation.Binary |
6 open import Data.Empty | 6 open import Data.Empty |
7 | 7 |
8 data One {n : Level } : Set n where | |
9 OneObj : One | |
10 | |
11 data Two : Set where | |
12 i0 : Two | |
13 i1 : Two | |
8 | 14 |
9 data Bool : Set where | 15 data Bool : Set where |
10 true : Bool | 16 true : Bool |
11 false : Bool | 17 false : Bool |
12 | 18 |