[Agda] splitting cases

[Andreas Abel]

Thorsten, I posted your question there

   https://github.com/agda/agda/issues/2858

and made a comment.

On 2020-03-31 13:04, Guillaume Allais wrote:
> Hi Thorsten
> 
> It is indeed already a feature request however it has not been implemented yet.
> It is quite non-trivial to do: https://github.com/agda/agda/issues/2858
> 
> Best,
> guillaume
> 
> 
> On 28/03/2020 16:16, Thorsten Altenkirch wrote:
>> Hi,
>>
>> I thought we were already able to split cases but it seems I was wrong:
>>
>> f : Bool → Bool
>>
>> f true = true
>>
>> b : Bool
>> b = false
>>
>> f false = b
>>
>> doesn’t work. Was this already a feature request? I actually need it mostly for pedagogical reasons. I want to prove a theorem, ah I need a lemma, let’s prove it and then continue.
>>
>> Yes, I know I could use with but this gets to complicated. However, splitting cases is also very useful for inductive-inductive definitions.
>>
>> Thorsten
>>
>>
>>
>> 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 contact the sender and delete the email and
>> attachment.
>>
>> Any views or opinions expressed by the author of this email do not
>> necessarily reflect the views of the University of Nottingham. Email
>> communications with the University of Nottingham may be monitored
>> where permitted by law.
>>
>>
>>
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>