Mercurial > hg > Members > atton > agda-proofs
annotate cbc/variable-tuple.agda @ 77:a2e6f61d5f2b default tip
Add modus-ponens
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 09 Feb 2017 06:32:03 +0000 |
parents | d503a73186ce |
children |
rev | line source |
---|---|
17 | 1 module variable-tuple where |
2 | |
3 open import Data.Nat hiding (_<_ ; _>_) | |
4 open import Data.String | |
5 open import Data.List | |
18
782a11f3eea4
Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
6 open import Data.Unit |
19
853318ff55f9
Trying define output data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
18
diff
changeset
|
7 open import Data.Product |
25
da78bb99d654
Embed function body to codesegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
8 open import Function using (_∘_ ; id) |
17 | 9 open import Relation.Binary.PropositionalEquality |
24
0fcb7b35ba81
Add data version CodeSegment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
22
diff
changeset
|
10 open import Level hiding (zero) |
17 | 11 |
12 data Format : Set₁ where | |
13 FEnd : Format | |
14 FSet : Set -> Format -> Format | |
15 | |
16 <> : Format | |
17 <> = FEnd | |
18 | |
19 infix 51 _> | |
20 _> : (Format -> Format) -> Format | |
21 _> f = f FEnd | |
22 | |
23 infixl 52 _||_ | |
24 _||_ : (Format -> Format) -> Set -> (Format -> Format) | |
25 _||_ f1 s = f1 ∘ (FSet s) | |
26 | |
18
782a11f3eea4
Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
27 infix 53 <_ |
17 | 28 <_ : Set -> Format -> Format |
29 <_ s = FSet s | |
30 | |
31 | |
32 unit : Format | |
33 unit = <> | |
34 | |
35 single : Format | |
36 single = < ℕ > | |
37 | |
38 double : Format | |
39 double = < String || ℕ > | |
40 | |
41 triple : Format | |
42 triple = < String || ℕ || (List ℕ) > | |
18
782a11f3eea4
Trying define input data segment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
43 |