<div dir="ltr"><div><div>0# and 1# are not constructors that you can match against. You can tell<br>from them being highlighted in a different colour than d1 and d2.<br></div><br></div><div>It wouldn't make sense to be able to match on 0# and 1# since depending<br></div><div><div>on the semiring they could be the same value, or have a type that doesn't<br></div><div>have decidable equality.<br></div><br></div><div>/ Ulf<br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, May 2, 2018 at 12:35 PM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Please, what is wrong in f' below? <br>
Why Agda-2.5.3 type-checks f and does not type-check f' ? <br>
<br>
------------------------------<wbr>---------------------------<br>
open import Level    using () renaming (zero to 0ℓ)<br>
open import Algebra  using (Semiring)<br>
open import Data.Nat using (ℕ)<br>
<br>
data Expr : Set  where c1 : ℕ → Expr<br>
                       c2 : Expr → Expr → Expr<br>
f : Expr → ℕ<br>
f (c1 _)        =  0<br>
f (c2 (c1 0) _) =  0<br>
f (c2 (c1 1) _) =  0<br>
f (c2 _      _) =  0<br>
<br>
postulate R : Semiring 0ℓ 0ℓ<br>
open Semiring R using (Carrier; 0#; 1#)<br>
<br>
data Expr' : Set  where d1 : Carrier → Expr'<br>
                        d2 : Expr' → Expr' → Expr'<br>
f' : Expr' → ℕ<br>
f' (d1 _)         =  0<br>
f' (d2 (d1 0#) _) =  0<br>
f' (d2 (d1 1#) _) =  0<br>
f' (d2 _       _) =  0<br>
------------------------------<wbr>----------------------------<br>
<br>
Agda reports  Unreachable clause  for the third pattern in  f',  as if<br>
it was shadowed by previous pattern. But it is not shadowed.<br>
<br>
Is this a bug in Agda-2.5.3 ?<br>
<br>
------<br>
Sergei  <br>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
</blockquote></div><br></div>