<div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote">On Sun, Jul 5, 2015 at 9:50 PM, Sergei Meshveliani <span dir="ltr">&lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Can anyone explain, please,<br>
what is the matter with the attached (small) code?<br>
<br>
It includes<br>
<br>
-----------------------------------------------------------------<br>
data DecPrime : ℕ → Set      -- constructively decided primality<br>
     where<br>
     prime    : {n : ℕ} → IsPrime n → DecPrime n<br>
     unity    : DecPrime 1<br>
     composed : {m n : ℕ} → IsNontrivialDivisor m n → DecPrime n<br>
<br>
postulate  decPrime : (n : ℕ) → DecPrime n<br>
<br>
f : ℕ → ℕ<br>
f n = g n (decPrime n)<br>
      where<br>
      g : (m : ℕ) → DecPrime m → ℕ<br>
<br>
      g 1 unity                = 1<br>
      g _ (prime _)            = 2<br>
      g _ (composed {k} {_} _) = k<br>
------------------------------------------------------------------<br></blockquote><div><br></div><div>The first and the second underscores must be the same. You&#39;ll get an easier to understand error if you replace the underscores with variables. This checks:</div><div><br></div><div>   g m (composed {k} {.m} _) = k</div><div><br></div><div>It would make more sense to make the first argument to g hidden though.</div><div><br></div><div>/ Ulf </div></div></div></div>