[Agda] Komencanta demando.

[Martin Stone Davis]

Saluton!

On line 34,

> ℕ⇨⟨Ω⟩ {zero″} zero = Ω-zero

zero″ is not a data constructor, so it's the same as

> ℕ⇨⟨Ω⟩ {whatever} zero = Ω-zero
If you change the line to

> ℕ⇨⟨Ω⟩ {whatever} zero = {!Ω-zero!}
and then C-u C-u C-c C-. in the hole, you'll see that you have ⟨ 0 , 0 
⟩, which does not unify with ⟨ whatever ⟩.

You could try something like

>   ℕ⇨⟨Ω⟩ : ∀ {ω} → ℕ → ⟨ ω ⟩
>   ℕ⇨⟨Ω⟩ {0 , 0} zero = Ω-zero
>   ℕ⇨⟨Ω⟩ {n , m} zero = {!!}
>   ℕ⇨⟨Ω⟩ (suc n) = Ω-next (ℕ⇨⟨Ω⟩ n)
though it's not yet clear to me what you'd want to write in the term of 
the second clause.

On 04/07/2016 04:25 AM, 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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160408/20f1f94a/attachment.html