[Agda] `with' to case_of_ example

[Sergei Meshveliani]

On Mon, 2016-05-09 at 14:50 +0000, Thorsten Altenkirch wrote:
> What is the difference between a proof and a function?
> 

I do not know, in general, I do not see a difference.
But the below message by Andreas is not about difference between a proof
and a function in general.
I think, it is about a certain relation between the two objects:
  a property  P  of the function  delKey,
  an implementation for a function that returns a proof for  P.

Regards,

------
Sergei


> On 06/05/2016, 13:47, "agda-bounces at lists.chalmers.se on behalf of Andreas
> Abel" <agda-bounces at lists.chalmers.se on behalf of
> andreas.abel at ifi.lmu.de> wrote:
> 
> >This is not a bug.
> >
> >As a rule of thumb, functions such as delKey can be implemented using
> >"case", but proofs about these functions usually need "with".
> >
> >On 04.05.2016 12:51, 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
> >>
> >
> >
> >-- 
> >Andreas Abel  <><      Du bist der geliebte Mensch.
> >
> >Department of Computer Science and Engineering
> >Chalmers and Gothenburg University, Sweden
> >
> >andreas.abel at gu.se
> >http://www2.tcs.ifi.lmu.de/~abel/
> >_______________________________________________
> >Agda mailing list
> >Agda at lists.chalmers.se
> >https://lists.chalmers.se/mailman/listinfo/agda
> 
> 
> 
> 
> 
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please send it back to me, and immediately delete it. 
> 
> Please do not use, copy or disclose the information contained in this
> message or in any attachment.  Any views or opinions expressed by the
> author of this email do not necessarily reflect the views of the
> University of Nottingham.
> 
> This message has been checked for viruses but the contents of an
> attachment may still contain software viruses which could damage your
> computer system, you are advised to perform your own checks. Email
> communications with the University of Nottingham may be monitored as
> permitted by UK legislation.
>