<html>
  <head>
    <meta content="text/html; charset=utf-8" http-equiv="Content-Type">
  </head>
  <body text="#000000" bgcolor="#FFFFFF">
    'ℕ⇨⟨Ω⟩ : ∀ {ω} → ℕ → ⟨ ω ⟩' 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, 'ℕ⇨⟨Ω⟩ : ℕ
    → ∃ λ ω → ⟨ ω ⟩':<br>
    <br>
    <blockquote type="cite">  ℕ⇨⟨Ω⟩ : ℕ → ∃ λ ω → ⟨ ω ⟩<br>
        ℕ⇨⟨Ω⟩ 0 = _ , Ω-zero<br>
        ℕ⇨⟨Ω⟩ (suc n) = _ , Ω-next (proj₂ (ℕ⇨⟨Ω⟩ n))<br>
    </blockquote>
    <br>
    <div class="moz-cite-prefix">On 04/08/2016 01:35 PM, Martin Stone
      Davis wrote:<br>
    </div>
    <blockquote cite="mid:5708160B.3080903@gmail.com" type="cite">
      <meta content="text/html; charset=utf-8" http-equiv="Content-Type">
      Saluton!<br>
      <br>
      On line 34,<br>
      <br>
      <blockquote type="cite">ℕ⇨⟨Ω⟩ {zero″} zero = Ω-zero<br>
      </blockquote>
      <br>
      zero″ is not a data constructor, so it's the same as<br>
      <br>
      <blockquote type="cite">ℕ⇨⟨Ω⟩ {whatever} zero = Ω-zero<br>
      </blockquote>
      If you change the line to<br>
      <br>
      <blockquote type="cite">ℕ⇨⟨Ω⟩ {whatever} zero = {!Ω-zero!}<br>
      </blockquote>
      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 ⟩.<br>
      <br>
      You could try something like<br>
      <br>
      <blockquote type="cite">  ℕ⇨⟨Ω⟩ : ∀ {ω} → ℕ → ⟨ ω ⟩<br>
          ℕ⇨⟨Ω⟩ {0 , 0} zero = Ω-zero<br>
          ℕ⇨⟨Ω⟩ {n , m} zero = {!!}<br>
          ℕ⇨⟨Ω⟩ (suc n) = Ω-next (ℕ⇨⟨Ω⟩ n)<br>
      </blockquote>
      though it's not yet clear to me what you'd want to write in the
      term of the second clause.<br>
      <br>
      <div class="moz-cite-prefix">On 04/07/2016 04:25 AM, Serge Leblanc
        wrote:<br>
      </div>
      <blockquote cite="mid:570643BB.2010501@gmail.com" type="cite">
        <meta http-equiv="content-type" content="text/html;
          charset=utf-8">
        Estimata al ĉiu<br>
        Dear all<br>
        <br>
        Kial tipa kontrolado tie malakceptas la 'zero = proj₁ zero″' 
        egalecon ?<br>
        Why type checking here rejects the 'zero = proj₁ zero″'
        equality?<br>
        <br>
        <font color="#3333ff">module Check where<br>
          <br>
          open import Data.Nat<br>
          open import Data.Product<br>
          <br>
          Ω = ℕ × ℕ<br>
          <br>
          zero″ : Ω<br>
          zero″ = (zero , zero)<br>
          <br>
          suc″ : Ω → Ω<br>
          suc″ (zero , y) = suc y , zero<br>
          suc″ (suc x , y) = x , suc y <br>
          <br>
          data ⟨_⟩ : Ω → Set where<br>
            Ω-zero : ⟨ zero″ ⟩<br>
            Ω-next : ∀ {ω} →  ⟨ ω ⟩ → ⟨ suc″ ω ⟩<br>
          <br>
          ℕ⇨⟨Ω⟩ : ∀ {ω} → ℕ → ⟨ ω ⟩<br>
          ℕ⇨⟨Ω⟩ {zero″} zero = Ω-zero<br>
          ℕ⇨⟨Ω⟩ (suc n) = Ω-next (ℕ⇨⟨Ω⟩ n)</font><br>
        <br>
        <font color="#000099">/home/serge/agda/Check.agda:34,22-28<br>
          zero != proj₁ zero″ of type ℕ<br>
          when checking that the expression Ω-zero has type ⟨ zero″ ⟩</font><br>
        <br>
        Sinceran dankon pro via venonta helpo.<br>
        Sincere thanks for your incoming help.<br>
        <div class="moz-signature">-- <br>
          Serge Leblanc
          <hr> gpg --keyserver hkp://keyserver.ubuntu.com:11371
          --recv-keys 0x67B17A3F <br>
          Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1
          7A3F </div>
        <br>
        <fieldset class="mimeAttachmentHeader"></fieldset>
        <br>
        <pre wrap="">_______________________________________________
Agda mailing list
<a moz-do-not-send="true" class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a moz-do-not-send="true" class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
      </blockquote>
      <br>
    </blockquote>
    <br>
  </body>
</html>