<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<style type="text/css" style="display:none;"><!-- P {margin-top:0;margin-bottom:0;} --></style>
</head>
<body dir="ltr">
<div id="divtagdefaultwrapper" style="font-size:12pt;color:#000000;font-family:Calibri,Helvetica,sans-serif;" dir="ltr">
<p style="margin-top:0;margin-bottom:0">just remove all R's from <font color="#3333ff">
parse″</font></p>
<p style="margin-top:0;margin-bottom:0"><font color="#3333ff"></font><br>
</p>
<p style="margin-top:0;margin-bottom:0"><font color="#3333ff"> parse′ : ∀ {R xs} → Parser R xs → Colist Char → Colist R<br>
parse′ {R} p₀ = parse″ p₀<br>
where<br>
parse″ : ∀ {xs} → Parser R xs → Colist Char → Colist R<br>
parse″ {xs = xs} p [] = Colist.fromList xs<br>
parse″ {xs = xs} p (t ∷ s) with t ≐ '\n'<br>
... | false = parse″ (∂ p t) (♭ s)<br>
... | true = (Colist.fromList xs) ++ (parse″ p₀ (♭ s))</font><br>
</p>
<p style="margin-top:0;margin-bottom:0"><br>
</p>
<div id="Signature">
<div id="divtagdefaultwrapper" dir="ltr" style="font-size: 12pt; color: rgb(0, 0, 0); font-family: Calibri, Arial, Helvetica, sans-serif, "EmojiFont", "Apple Color Emoji", "Segoe UI Emoji", NotoColorEmoji, "Segoe UI Symbol", "Android Emoji", EmojiSymbols;">
<div><font style="font-size:12pt" size="3"><span style="color:rgb(69,129,142)"><span style="font-family:trebuchet ms,sans-serif"><b>Sincerely Yours,<br>
</b></span></span></font></div>
<font style="font-size:12pt" size="3"><span style="color:rgb(69,129,142)"><span style="font-family:trebuchet ms,sans-serif"><b><br>
Jason Hu<a target="_blank" id="LPNoLP"></a></b></span></span></font> </div>
</div>
</div>
<hr style="display:inline-block;width:98%" tabindex="-1">
<div id="divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" style="font-size:11pt" color="#000000"><b>From:</b> Agda <agda-bounces@lists.chalmers.se> on behalf of Serge Leblanc <33dbqnxpy7if@gmail.com><br>
<b>Sent:</b> September 13, 2018 11:01:48 AM<br>
<b>To:</b> agda@lists.chalmers.se<br>
<b>Subject:</b> [Agda] Type mismatch? Tipo miskongruas?</font>
<div> </div>
</div>
<meta content="text/html; charset=utf-8">
<div style="background-color:#FFFFFF">Dear all, how do indicate that p₀ and p have the same type in this above example? Apparently, {R = R} is not enough.<br>
Estimata ĉiuj, kiel oni indikas ke p₀ kaj p havas la saman tipon en ĉi supra ekzemplo ? Ŝajne, {R = R} ne sufiŝas.<br>
<p><font color="#3333ff"> {-# NON_TERMINATING #-}<br>
parse′ : ∀ {R xs} → Parser R xs → Colist Char → Colist R<br>
parse′ {R} p₀ = parse″ p₀<br>
where<br>
parse″ : ∀ {R xs} → Parser R xs → Colist Char → Colist R<br>
parse″ {xs = xs} p [] = Colist.fromList xs<br>
parse″ {R = R}{xs = xs} p (t ∷ s) with t ≐ '\n'<br>
... | false = parse″ (∂ p t) (♭ s)<br>
... | true = (Colist.fromList xs) ++ (parse″ p₀ (♭ s))</font></p>
<p>Sinceran dankon pro via venonta helpo.<br>
</p>
<p>-- <br>
</p>
<div class="x_moz-signature">Serge Leblanc
<hr>
gpg --search-keys 0x67B17A3F <br>
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F</div>
</div>
</body>
</html>