Mercurial > hg > Members > atton > agda-proofs

comparison cbc/variable-tuple.agda @ 20:4dd4400b48aa

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Define code segment execution
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Sun, 18 Dec 2016 08:10:02 +0000
parents 853318ff55f9
children 84e3fbc662db
comparison
equal deleted inserted replaced
19:853318ff55f9 20:4dd4400b48aa
64 ids {A} (cs i o) = DataSegment {A} i 64 ids {A} (cs i o) = DataSegment {A} i
65 65
66 ids-double : {A : Set} {a : A} -> ids {A} csDouble 66 ids-double : {A : Set} {a : A} -> ids {A} csDouble
67 ids-double {_} {a} = \(s : String) -> \(n : ℕ) -> a 67 ids-double {_} {a} = \(s : String) -> \(n : ℕ) -> a
68 68
69
70 executeCS : (cs : CodeSegment) -> Set
71 executeCS c = ids {ods c} c
72