Mercurial > hg > Gears > GearsAgda

comparison logic.agda @ 950:5c75fc6dfe59

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 Tue, 13 Aug 2024 23:03:40 +0900
parents 057d3309ed9d
children
comparison
equal deleted inserted replaced
949:057d3309ed9d 950:5c75fc6dfe59
89 data Dec0 {n : Level} (A : Set n) : Set n where 89 data Dec0 {n : Level} (A : Set n) : Set n where
90 yes0 : A → Dec0 A 90 yes0 : A → Dec0 A
91 no0 : (A → ⊥) → Dec0 A 91 no0 : (A → ⊥) → Dec0 A
92 92
93 open _∧_ 93 open _∧_
94 ∧-injective : {n m : Level} {A : Set n} {B : Set m} → {a b : A ∧ B} → proj1 a ≡ proj1 b → proj2 a ≡ proj2 b → a ≡ b 94 ∧-uniue : {n m : Level} {A : Set n} {B : Set m} → {a b : A ∧ B} → proj1 a ≡ proj1 b → proj2 a ≡ proj2 b → a ≡ b
95 ∧-injective refl refl = refl 95 ∧-uniue refl refl = refl
96 96
97 not-not-bool : { b : Bool } → not (not b) ≡ b 97 not-not-bool : { b : Bool } → not (not b) ≡ b
98 not-not-bool {true} = refl 98 not-not-bool {true} = refl
99 not-not-bool {false} = refl 99 not-not-bool {false} = refl
100 100