17
|
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 ℕ) >
|