<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"><<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">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'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>