[Agda] Implicit arguments inference

[Valery Isaev]

Oh, sorry. It seems that this code works well indeed. The problem occurs in
the code I give below. The reason is that I import both Data.List and
Data.Vec. But since xs has type List ℕ, it should be obvious which
constructor to use.
PS: I'm using Agda 2.5.1.1.

open import Data.Nat
open import Data.Vec
open import Data.List
open import Relation.Binary.PropositionalEquality

A : (xs : List ℕ) → Set
A xs = 0 ∷ xs ≡ 0 ∷ xs

Regards,
Valery Isaev

2016-09-26 7:27 GMT+03:00 Roman <effectfully at gmail.com>:

> My Agda (version 2.6.0) infers everything properly.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160926/3c5582f3/attachment.html