[Agda] Komencanta demando.

[Martin Stone Davis]

'ℕ⇨⟨Ω⟩ : ∀ {ω} → ℕ → ⟨ ω ⟩' says that for any ω and any ℕ, we can 
produce a ⟨ ω ⟩. I'm guessing what you really want to say is that for 
any ℕ, there is an ω such that ⟨ ω ⟩. In other words, 'ℕ⇨⟨Ω⟩ : ℕ → ∃ λ ω 
→ ⟨ ω ⟩':

>   ℕ⇨⟨Ω⟩ : ℕ → ∃ λ ω → ⟨ ω ⟩
>   ℕ⇨⟨Ω⟩ 0 = _ , Ω-zero
>   ℕ⇨⟨Ω⟩ (suc n) = _ , Ω-next (proj₂ (ℕ⇨⟨Ω⟩ n))

On 04/08/2016 01:35 PM, Martin Stone Davis wrote:
> 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/b0333c24/attachment.html