[Agda] `with' question

[Martin Stone Davis]

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 [].

g' : Dec (f ps ≡ 1)
g'
   with ps | null? ps
... | ._ | yes null-ps =  yes (h null-ps)


--
Martin Stone Davis

Postal/Residential:
1223 Ferry St
Apt 5
Eugene, OR 97401
Talk / Text / Voicemail: (310) 699-3578 <3106993578>
Electronic Mail: martin.stone.davis at gmail.com
Website: martinstonedavis.com

On Fri, Feb 5, 2016 at 12:34 PM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

> Please, what is wrong in the below program?
>
> -----------------------------------------------------------
> module Useful where
> open import Relation.Nullary using (Dec; yes; no)
> open import Relation.Binary.PropositionalEquality as PE using (_≡_; _≢_)
> open import Data.Nat   using (ℕ)
> open import Data.List  using (List; []; _∷_)
>
> --------------------------------------------------------
> module _ {α} {A : Set α}
>     where
>     data Null : List A → Set α  where  isNull : Null []
>
>     null? :  (xs : List A) → Dec (Null xs)
>     null? []      = yes isNull
>     null? (_ ∷ _) = no λ()
>
> --------------------------------------------------------
> f : List ℕ  → ℕ
> f []      =  1
> f (_ ∷ _) =  0
>
> postulate  ps : List ℕ
>
> g : Dec (f ps ≡ 1)
> g with null? ps
> ... | yes null-ps =  yes (h null-ps)
> ... | no _        =  no neq
>                      where
>                      postulate neq : f ps ≢ 1
>
> g' : Dec (f ps ≡ 1)
> g'
>    with ps | null? ps
> ... | _ | yes null-ps =  yes (h null-ps)
> ... | _ | no _        =  no neq
>                          where
>                          postulate neq : f ps ≢ 1
> --------------------------------------------------------------------
>
> g  is type-checked,
> and for  g'  it reports that  null-ps  has not the needed type.
>
> (The Agda language is difficult in its proof composition part.
> I do not understand basics of Agda after 3 year practicing with it).
>
> In this example, the part  "ps |"  is dummy.
> But in the real example I need to use both  ps  and  null? ps,
> like this:
>
>   ... | []           | null-ps =  foo null-ps
>   ... | (_ , 0) :: _ | _       =  \bot-elim ... 0>0
>   ...
>
> g'  is a simplification for this real example.
>
> Thank you in advance for explanation,
>
> ------
> Sergei
>
>
>
>
> _______________________________________________
> 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/20160205/28779686/attachment.html