[Agda] splitting cases

[Guillaume Allais]

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
>