-- Autumn school "Proof and Computation"
-- 3-8 October 2016
-- Fischbachau, Bayern, DE
--
--   Andreas Abel, Agda Tutorial
--
-- Part 2: Formal languages, coinductively treated via copatterns

module Copatterns where

open import Data.Nat.Base
open import Data.Bool.Base

open import Relation.Binary.PropositionalEquality

open import Size


module Streams where

  -- Streams

  -- Repetition

  -- Stream zipping

  -- Fibonacci

module SizedStreams where


module Languages where

  -- Decidable language

  record Lang (A : Set) : Set where

  -- empty language

  ∅ : ∀{A} → Lang A
  ∅ = {!!}

  -- empty word

  ε : ∀{A} → Lang A
  ε = {!!}

  -- union

  infixl  4 _∪_

  _∪_ : ∀{A} (l k : Lang A) → Lang A
  l ∪ k = {!!}

  -- concatenation

  infixl  6 _∙_

  _∙_ : ∀{A} (l k : Lang A) → Lang A
  l ∙ k = {!!}

  -- star
  infixr 15 _*

  _* : ∀{A} (l : Lang A) → Lang A
  l * = {!!}

module SizedLanguages where