[Agda] type inference error?

[Darryl]

To my knowledge, Agda has basically *never* had (or never had reliable) constructor disambiguation. Anyone using Nat and Level will have experienced this.
 
- darryl



________________________________
 
Hi,

Is the following a known error in Agda?
My student have found this.

---------------------------------------
data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

data ⊥ : Set where
  suc : ⊥ → ⊥

-- it looks like Agda can't tell (suc : ℕ → ℕ) apart from the other suc
-- this is unreasonable: the type of suc should be inferred from the
-- fact that (x : ℕ)

lemma : (x : ℕ) → suc x ≡ suc x
lemma _ = refl
---------------------------------------


Peter
_______________________________________________
Agda mailing list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130109/33c0a828/attachment.html