Mercurial > hg > Members > atton > agda-proofs

comparison cbc/subtype-sample.agda @ 52:4880184e4ab5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Define push/pop using subtype
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Tue, 10 Jan 2017 09:04:55 +0000
parents 16e27df74ec5
children
comparison
equal deleted inserted replaced
51:16e27df74ec5 52:4880184e4ab5
13 cycle : ℕ 13 cycle : ℕ
14 led : String 14 led : String
15 signature : String 15 signature : String
16 16
17 open import subtype Context 17 open import subtype Context
18
19
18 record LoopCounter : Set where 20 record LoopCounter : Set where
19 field 21 field
20 count : ℕ 22 count : ℕ
21 name : String 23 name : String
22 24