Mercurial > hg > Members > Moririn

diff 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
line wrap: on
line diff
--- a/logic.agda	Wed Nov 03 18:28:31 2021 +0900
+++ b/logic.agda	Thu Nov 04 16:35:11 2021 +0900
@@ -14,6 +14,7 @@
     false : Bool
 
 record  _∧_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
+   constructor ⟪_,_⟫
    field
       proj1 : A
       proj2 : B