Mercurial > hg > Members > atton > agda-proofs

comparison 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
comparison
equal deleted inserted replaced
26:d503a73186ce 27:892f8b3aa57e
4 open import Data.Product 4 open import Data.Product
5 open import Data.Nat 5 open import Data.Nat
6 open import Function using (_∘_ ; id) 6 open import Function using (_∘_ ; id)
7 open import Data.Unit 7 open import Data.Unit
8 8
9 data CodeSegment (I O : Set) : Set₁ where 9 data CodeSegment (I O : Set) : Set where
10 cs : (I -> O) -> CodeSegment I O 10 cs : (I -> O) -> CodeSegment I O
11 11
12 12
13 twiceWithName : (String × ℕ ) -> (String × ℕ ) 13 twiceWithName : (String × ℕ ) -> (String × ℕ )
14 twiceWithName (s , n) = s , twice n 14 twiceWithName (s , n) = s , twice n