[Agda] `with' to case_of_ example

[Sergei Meshveliani]

There is a simpler example in the same environment. The function

  eq :  ∀ k v (ps : List Pair) → delKey k ((k , v) ∷ ps) ≡ ps
  eq k _ _ 
           with k ≟ k
  ...      | yes _  = PE.refl
  ...      | no k≉k = ⊥-elim (k≉k refl)

is type-checked, and 

  	   = case k ≟ k of \ { (yes _)  → PE.refl
                             ; (no k≉k) → ⊥-elim (k≉k refl) }
is not.
May be it needs lifting of ⊥ to somewhere, I do not know.



On Wed, 2016-05-04 at 14:51 +0400, Sergei Meshveliani wrote:
> Hi, all,
> 
> I attach a small program for deleting a key from a pair list,
> and for proving  (Preserves _≈_ ⟶ _≡_)  for this operation.
> 
> The `with' version is type-checked and the `case' version is not
> (Agda 2.5.1, ghc-7.10.2).
> 
> Is this a bug?
> Can it be written as case_of_ ? 
> 
> (Agda 2.5.1, ghc-7.10.2).
> 
> Thanks,
> 
> ------
> Sergei
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda