agda/test/LaTeXAndHTML/succeed/Issue1062.lagda

\nonstopmode
\documentclass{article}

\usepackage{agda}

\begin{document}
\begin{code}

{-# OPTIONS --copatterns --sized-types #-}

{-# BUILTIN SIZE    Size   #-}
{-# BUILTIN SIZELT  Size<_ #-}
{-# BUILTIN SIZESUC ↑_     #-}
{-# BUILTIN SIZEINF ∞      #-}

data List (A : Set) : Set where
  [] : List A
  _∷_ : (x : A) (xs : List A) -> List A

record _×_ (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B
open _×_

-- Sized streams via head/tail.

record Stream {i : Size} (A : Set) : Set where
  coinductive; constructor _∷_
  field
    head  : A
    tail  : ∀ {j : Size< i} → Stream {j} A
open Stream public

_∷ˢ_ : ∀ {i A} → A → Stream {i} A → Stream {↑ i} A
head  (a ∷ˢ as) = a
tail  (a ∷ˢ as) = as

-- Streams and lists.

-- Prepending a list to a stream.

_++ˢ_ : ∀ {i A} → List A → Stream {i} A → Stream {i} A
[]        ++ˢ s = s
(a ∷ as)  ++ˢ s = a ∷ˢ (as ++ˢ s)

-- Unfold which produces several outputs at one step

record List1 (A : Set) : Set where
  constructor _∷_
  field
    head  : A
    tail  : List A
open List1 using (head; tail)

record ⊤ : Set where constructor trivial
open List1 (trivial ∷ []) using (head; tail) -- problem: imports not colored

unfold⁺ : ∀ {S : Size → Set} {A : Set}

  (step : ∀ {i} → S i → List1 A × (∀ {j : Size< i} → S j)) →

  ∀ {i} → (s : S i) → Stream {i} A

head  (unfold⁺ step s) =  head (fst (step s))
tail  (unfold⁺ step s) =  let  ((_ ∷ l) , s′) = step s
                          in   l ++ˢ unfold⁺ step s′
\end{code}
Problem: The ∷ in the last let statement is not colored with constructor color.
\end{document}