[Agda] Komencenta demando.

[Guillaume Brunerie]

On 2015-11-25 19:43 GMT+01:00 Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> See attached file.
>
> I have never seen your language, but I think I guessed correctly...

(it’s Esperanto)

> Cheers,
> Andreas
>
>
> On 25.11.2015 16:14, Serge Leblanc wrote:
>>
>> Ĉu iu bondeziras indiki al mi kiel oni uzas _≡[_]_ ?
>> Does anyone wish to indicate to me how to use _≡ [_] _?
>>
>> Dankon.
>> Thanks.
>>
>>
>> On 2015-11-19 16:33, Serge Leblanc wrote:
>>>
>>> Estimata ĉiuj,
>>>
>>> En funkcio 'suc-conv' mi ne scias kiamaniere indiki la komutecon de
>>> adico (+-comm). Verŝajne, ni uzas egalan rezonon enkondukite de
>>> _≡[_]_, ĉu ne ? Bedaūrinde, mi ne komprenas kiel uzi ĝin!
>>>
>>> Bonvolu indiki al mi kiel fari ?
>>> Sincere,
>>>
>>>
>>> Dear all,
>>>
>>> In function 'suc-conv' I don't know how to indicate the commutativity
>>> of addition (+-comm). Probably, we use an equal argument introduced
>>> from _≡ [_] _, is not it? Unfortunately, I don't understand how to use
>>> it!
>>>
>>> Could you tell me howto do?
>>> Sincerely,
>>>
>>>
>>>
>>> module Recursive where
>>>
>>> open import Data.Nat
>>> open import Data.Nat.Properties.Simple using (+-comm)
>>> open import Relation.Binary.PropositionalEquality as PropEq using
>>> (_≡_; refl; cong; cong₂)
>>> open PropEq.≡-Reasoning renaming (_≡⟨_⟩_ to _≡[_]_)
>>>
>>> data ℕ⁰ : Set where
>>>   zero : ℕ⁰
>>>   2k : ℕ⁰ → ℕ⁰
>>>   2k+1 : ℕ⁰ → ℕ⁰
>>>
>>> suc⁰ : ℕ⁰ → ℕ⁰
>>> suc⁰ zero = 2k+1 zero
>>> suc⁰ (2k n) = 2k+1 n
>>> suc⁰ (2k+1 n) = 2k (suc⁰ n)
>>>
>>> conv⁰→ : ℕ⁰ → ℕ
>>> conv⁰→ zero = zero
>>> conv⁰→ (2k n) = conv⁰→ n + conv⁰→ n
>>> conv⁰→ (2k+1 n) = suc (conv⁰→ n + conv⁰→ n)
>>>
>>> conv⁰← : ℕ → ℕ⁰
>>> conv⁰← zero = zero
>>> conv⁰← (suc n) = suc⁰ (conv⁰← n)
>>>
>>> suc-conv : (n : ℕ⁰) → conv⁰→ (suc⁰ n) ≡ suc (conv⁰→ n)
>>> suc-conv zero = refl
>>> suc-conv (2k n) = refl
>>> suc-conv (2k+1 n) = {! cong₂ _+_  (suc-conv n) (suc-conv n) !}
>>>
>>> --
>>> Serge Leblanc
>>> ------------------------------------------------------------------------
>>> gpg --keyserver hkp://keyserver.ubuntu.com:11371 --recv-keys 0x67B17A3F
>>> Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
>>
>>
>> --
>> 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/
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>