<html><body><div style="color:#000; background-color:#fff; font-family:arial, helvetica, sans-serif;font-size:10pt"><div><span>To my knowledge, Agda has basically *never* had (or never had reliable) constructor disambiguation. Anyone using Nat and Level will have experienced this.</span></div><div></div><div> </div><div>- darryl<br></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><br></div> <div style="font-family: arial, helvetica, sans-serif; font-size: 10pt; "> <div style="font-family: 'times new roman', 'new york', times, serif; font-size: 12pt; "> <div dir="ltr"> <font size="2" face="Arial"> <hr size="1"> </font></div><div style="font-family: times new roman, new york, times, serif; font-size: 12pt;" class="yui_3_7_2_18_1357752605059_61"><br></div>Hi,<br><br>Is the following a known error in Agda?<br>My student have found
this.<br><br>---------------------------------------<br>data ℕ : Set where<br> zero : ℕ<br> suc : ℕ → ℕ<br><br>data _≡_ {A : Set} (x : A) : A → Set where<br> refl : x ≡ x<br><br>data ⊥ : Set where<br> suc : ⊥ → ⊥<br><br>-- it looks like Agda can't tell (suc : ℕ → ℕ) apart from the other suc<br>-- this is unreasonable: the type of suc should be inferred from the<br>-- fact that (x : ℕ)<br><br>lemma : (x : ℕ) → suc x ≡ suc x<br>lemma _ = refl<br>---------------------------------------<br><br><br>Peter<br>_______________________________________________<br>Agda mailing list<br><a ymailto="mailto:Agda@lists.chalmers.se" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br><a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br><br><br> </div> </div> </div></body></html>