[Agda] Type mismatch? Tipo miskongruas?

[Nils Anders Danielsson]

On 2018-09-13 17:01, Serge Leblanc wrote:
> {-# NON_TERMINATING #-}
> parse′ : ∀ {R xs} → Parser R xs → Colist Char → Colist R
> parse′ {R} p₀ = parse″ p₀
>   where
>     parse″ : ∀ {R xs} → Parser R xs → Colist Char → Colist R
>     parse″ {xs = xs} p [] = Colist.fromList xs
>     parse″ {R = R}{xs = xs} p (t ∷ s) with t ≐ '\n'
>     ... | false = parse″ (∂ p t) (♭ s)
>     ... | true = (Colist.fromList xs) ++ (parse″ p₀ (♭ s))
>
> main = run $ ♯ getContents >>=IO
>   λ s → ♯ mapM′ (putStrLn ∘ showExpr) (parse′ term s)

One way to avoid using NON_TERMINATING would be to use
IO.readFiniteFile.

-- 
/NAD