Mercurial > hg > Members > atton > agda-proofs

diff cbc/product.agda @ 27:892f8b3aa57e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ReWrite stack.agda using product type definition
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Fri, 23 Dec 2016 10:20:05 +0000
parents d503a73186ce
children dc6a09d4f900
line wrap: on
line diff
--- a/cbc/product.agda	Fri Dec 23 02:50:03 2016 +0000
+++ b/cbc/product.agda	Fri Dec 23 10:20:05 2016 +0000
@@ -6,7 +6,7 @@
 open import Function using (_∘_ ; id)
 open import Data.Unit
 
-data CodeSegment (I O : Set) : Set₁ where
+data CodeSegment (I O : Set) : Set where
   cs : (I -> O) -> CodeSegment I O