[Agda] Komencanta demando.

[Andreas Abel]

Because the zero'' in that clause is a variable, not the zero'' you 
defined above.  If you want to match against the defined zero'', you 
have to turn it into a pattern synonym.

open import Data.Nat
open import Data.Product

Ω = ℕ × ℕ

pattern zero″ = (zero , zero)

suc″ : Ω → Ω
suc″ (zero , y) = suc y , zero
suc″ (suc x , y) = x , suc y

data ⟨_⟩ : Ω → Set where
   Ω-zero : ⟨ zero″ ⟩
   Ω-next : ∀ {ω} →  ⟨ ω ⟩ → ⟨ suc″ ω ⟩

ℕ⇨⟨Ω⟩ : ∀ {ω} → ℕ → ⟨ ω ⟩
ℕ⇨⟨Ω⟩ {zero″} zero = Ω-zero
ℕ⇨⟨Ω⟩ (suc n) = Ω-next (ℕ⇨⟨Ω⟩ n)

But then you get a different error (incomplete pattern matching), which 
is not surprising.

Cheers,
Andreas

On 07.04.2016 13:25, Serge Leblanc wrote:
> Estimata al ĉiu
> Dear all
>
> Kial tipa kontrolado tie malakceptas la 'zero = proj₁ zero″' egalecon ?
> Why type checking here rejects the 'zero = proj₁ zero″' equality?
>
> module Check where
>
> open import Data.Nat
> open import Data.Product
>
> Ω = ℕ × ℕ
>
> zero″ : Ω
> zero″ = (zero , zero)
>
> suc″ : Ω → Ω
> suc″ (zero , y) = suc y , zero
> suc″ (suc x , y) = x , suc y
>
> data ⟨_⟩ : Ω → Set where
>    Ω-zero : ⟨ zero″ ⟩
>    Ω-next : ∀ {ω} →  ⟨ ω ⟩ → ⟨ suc″ ω ⟩
>
> ℕ⇨⟨Ω⟩ : ∀ {ω} → ℕ → ⟨ ω ⟩
> ℕ⇨⟨Ω⟩ {zero″} zero = Ω-zero
> ℕ⇨⟨Ω⟩ (suc n) = Ω-next (ℕ⇨⟨Ω⟩ n)
>
> /home/serge/agda/Check.agda:34,22-28
> zero != proj₁ zero″ of type ℕ
> when checking that the expression Ω-zero has type ⟨ zero″ ⟩
>
> Sinceran dankon pro via venonta helpo.
> Sincere thanks for your incoming help.
> --
> Serge Leblanc
> ------------------------------------------------------------------------
> gpg --keyserver hkp://keyserver.ubuntu.com:11371 --recv-keys 0x67B17A3F
> Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/