<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>