Mercurial > hg > Members > atton > agda-proofs

comparison cbc/variable-tuple.agda @ 17:7bfae9affc84

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add variable-tuple
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Sun, 18 Dec 2016 01:35:31 +0000
parents
children 782a11f3eea4
comparison
equal deleted inserted replaced
16:62dfa11a8629 17:7bfae9affc84
1 module variable-tuple where
2
3 open import Data.Nat hiding (_<_ ; _>_)
4 open import Data.String
5 open import Data.List
6 open import Function using (_∘_)
7 open import Relation.Binary.PropositionalEquality
8
9 data Format : Set₁ where
10 FEnd : Format
11 FSet : Set -> Format -> Format
12
13 <> : Format
14 <> = FEnd
15
16 {-
17 begin_ : ∀{x y : A} → x ≡ y → x ≡ y
18 begin_ x≡y = x≡y
19
20 _≡⟨⟩_ : ∀ (x {y} : A) → x ≡ y → x ≡ y
21 _ ≡⟨⟩ x≡y = x≡y
22
23 _≡⟨_⟩_ : ∀ (x {y z} : A) → x ≡ y → y ≡ z → x ≡ z
24 _ ≡⟨ x≡y ⟩ y≡z = trans x≡y y≡z
25
26 _≅⟨_⟩_ : ∀ (x {y z} : A) → x ≅ y → y ≡ z → x ≡ z
27 _ ≅⟨ x≅y ⟩ y≡z = trans (H.≅-to-≡ x≅y) y≡z
28
29 _∎ : ∀ (x : A) → x ≡ x
30 _∎ _ = refl
31 -}
32
33 infix 51 _>
34 _> : (Format -> Format) -> Format
35 _> f = f FEnd
36
37 infixl 52 _||_
38 _||_ : (Format -> Format) -> Set -> (Format -> Format)
39 _||_ f1 s = f1 ∘ (FSet s)
40
41 infix 54 <_
42 <_ : Set -> Format -> Format
43 <_ s = FSet s
44
45
46 unit : Format
47 unit = <>
48
49 single : Format
50 single = < ℕ >
51
52 double : Format
53 double = < String || ℕ >
54
55 triple : Format
56 triple = < String || ℕ || (List ℕ) >