<div dir="ltr">You didn't include the definition of h, so it's hard to check for sure, but my guess is that you need a dot-pattern on the yes line of g', because ps is inferred as [].<br><br>g' : Dec (f ps ≡ 1)<br>
g'<br>
with ps | null? ps<br>
... | ._ | yes null-ps = yes (h null-ps)<br>
<br></div><div class="gmail_extra"><br clear="all"><div><div class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr">--<br>Martin Stone Davis<br><div><br>Postal/Residential:<br></div><div style="margin-left:40px"><span>1223 Ferry St</span><span><span><br></span></span></div><div style="margin-left:40px"><span><span>Apt 5<br></span></span></div><div style="margin-left:40px"><span>Eugene, OR 97401</span><br></div>Talk / <span></span>Text / Voicemail: <a href="tel:3106993578" value="+13106993578" target="_blank">(310) 699-3578</a><br>Electronic Mail: <a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a><div><div><div><span></span></div></div></div></div></div><div dir="ltr"><span style="font-size:small">Website: </span><a href="http://martinstonedavis.com/" style="color:rgb(17,85,204);font-size:small" target="_blank">martinstonedavis.com</a></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div>
<br><div class="gmail_quote">On Fri, Feb 5, 2016 at 12:34 PM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Please, what is wrong in the below program?<br>
<br>
-----------------------------------------------------------<br>
module Useful where<br>
open import Relation.Nullary using (Dec; yes; no)<br>
open import Relation.Binary.PropositionalEquality as PE using (_≡_; _≢_)<br>
open import Data.Nat using (ℕ)<br>
open import Data.List using (List; []; _∷_)<br>
<br>
--------------------------------------------------------<br>
module _ {α} {A : Set α}<br>
where<br>
data Null : List A → Set α where isNull : Null []<br>
<br>
null? : (xs : List A) → Dec (Null xs)<br>
null? [] = yes isNull<br>
null? (_ ∷ _) = no λ()<br>
<br>
--------------------------------------------------------<br>
f : List ℕ → ℕ<br>
f [] = 1<br>
f (_ ∷ _) = 0<br>
<br>
postulate ps : List ℕ<br>
<br>
g : Dec (f ps ≡ 1)<br>
g with null? ps<br>
... | yes null-ps = yes (h null-ps)<br>
... | no _ = no neq<br>
where<br>
postulate neq : f ps ≢ 1<br>
<br>
g' : Dec (f ps ≡ 1)<br>
g'<br>
with ps | null? ps<br>
... | _ | yes null-ps = yes (h null-ps)<br>
... | _ | no _ = no neq<br>
where<br>
postulate neq : f ps ≢ 1<br>
--------------------------------------------------------------------<br>
<br>
g is type-checked,<br>
and for g' it reports that null-ps has not the needed type.<br>
<br>
(The Agda language is difficult in its proof composition part.<br>
I do not understand basics of Agda after 3 year practicing with it).<br>
<br>
In this example, the part "ps |" is dummy.<br>
But in the real example I need to use both ps and null? ps,<br>
like this:<br>
<br>
... | [] | null-ps = foo null-ps<br>
... | (_ , 0) :: _ | _ = \bot-elim ... 0>0<br>
...<br>
<br>
g' is a simplification for this real example.<br>
<br>
Thank you in advance for explanation,<br>
<br>
------<br>
Sergei<br>
<br>
<br>
<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div>