# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1482024931 0
# Node ID 7bfae9affc84682c95fb5b68644f47e779a17d86
# Parent  62dfa11a8629fe902ae05b87e0030ddb4c79f169
Add variable-tuple

diff -r 62dfa11a8629 -r 7bfae9affc84 cbc/variable-tuple.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/cbc/variable-tuple.agda	Sun Dec 18 01:35:31 2016 +0000
@@ -0,0 +1,56 @@
+module variable-tuple where
+
+open import Data.Nat hiding (_<_ ; _>_)
+open import Data.String
+open import Data.List
+open import Function using (_∘_)
+open import Relation.Binary.PropositionalEquality
+
+data Format : Set₁ where
+  FEnd : Format
+  FSet : Set -> Format -> Format
+
+<> : Format
+<> = FEnd
+
+{-
+  begin_ : ∀{x y : A} → x ≡ y → x ≡ y
+  begin_ x≡y = x≡y
+
+  _≡⟨⟩_ : ∀ (x {y} : A) → x ≡ y → x ≡ y
+  _ ≡⟨⟩ x≡y = x≡y
+
+  _≡⟨_⟩_ : ∀ (x {y z} : A) → x ≡ y → y ≡ z → x ≡ z
+  _ ≡⟨ x≡y ⟩ y≡z = trans x≡y y≡z
+
+  _≅⟨_⟩_ : ∀ (x {y z} : A) → x ≅ y → y ≡ z → x ≡ z
+  _ ≅⟨ x≅y ⟩ y≡z = trans (H.≅-to-≡ x≅y) y≡z
+
+  _∎ : ∀ (x : A) → x ≡ x
+  _∎ _ = refl
+-}
+
+infix  51 _>
+_> : (Format -> Format) -> Format
+_> f = f FEnd
+
+infixl 52 _||_
+_||_ : (Format -> Format) -> Set -> (Format -> Format)
+_||_ f1 s = f1 ∘ (FSet s)
+
+infix 54 <_
+<_ : Set -> Format -> Format
+<_ s = FSet s
+
+
+unit : Format
+unit = <>
+
+single : Format
+single = < ℕ  >
+
+double : Format
+double = < String || ℕ  >
+
+triple : Format
+triple = < String || ℕ  || (List ℕ) >