------------------------------------------------------------------------
-- Booleans
------------------------------------------------------------------------

{-# OPTIONS --guardedness #-}

module Examples.Bool where

open import Codata.Musical.Notation
open import Data.Bool
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

open import Grammar.Infinite using (Grammar)
import Pretty
open import Renderer

module _ where

  open Grammar.Infinite

  bool : Grammar Bool
  bool = true  <$ string′ "true"
       ∣ false <$ string′ "false"

open Pretty

bool-printer : Pretty-printer bool
bool-printer true  = left  (<$ text)
bool-printer false = right (<$ text)

test₁ : render 4 (bool-printer true) ≡ "true"
test₁ = refl

test₂ : render 0 (bool-printer false) ≡ "false"
test₂ = refl
