[Agda] Type mismatch? Tipo miskongruas?

[Jason -Zhong Sheng- Hu]

just remove all R's from parse″


  parse′ : ∀ {R xs} → Parser R xs → Colist Char → Colist R
  parse′ {R} p₀ = parse″ p₀
    where
      parse″ : ∀ {xs} → Parser R xs → Colist Char → Colist R
      parse″ {xs = xs} p [] = Colist.fromList xs
      parse″ {xs = xs} p (t ∷ s) with t ≐ '\n'
      ... | false = parse″ (∂ p t) (♭ s)
      ... | true = (Colist.fromList xs) ++ (parse″ p₀ (♭ s))


Sincerely Yours,

Jason Hu
________________________________
From: Agda <agda-bounces at lists.chalmers.se> on behalf of Serge Leblanc <33dbqnxpy7if at gmail.com>
Sent: September 13, 2018 11:01:48 AM
To: agda at lists.chalmers.se
Subject: [Agda] Type mismatch? Tipo miskongruas?

Dear all, how do indicate that p₀ and p have the same type in this above example? Apparently, {R = R} is not enough.
Estimata ĉiuj, kiel oni indikas ke p₀ kaj p havas la saman tipon en ĉi supra ekzemplo ? Ŝajne, {R = R} ne sufiŝas.

  {-# 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))

Sinceran dankon pro via venonta helpo.

--

Serge Leblanc
________________________________
gpg --search-keys 0x67B17A3F
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180913/fd9fb557/attachment.html>