Stream: math-comp users

Topic: ✔ case_eq in SSR style


view this post on Zulip Vincent Siles (Nov 10 2021 at 13:10):

Hi ! What would be the SSR way to do case_eq (my_complex_expression) ?

view this post on Zulip Karl Palmskog (Nov 10 2021 at 13:11):

I think you want case hypname: (my_complex_expression) generally

view this post on Zulip Christian Doczkal (Nov 10 2021 at 13:15):

In the simplest form that's correct. For more, have a look at equation generation in the manual.

view this post on Zulip Enrico Tassi (Nov 10 2021 at 13:16):

You may want to case hyp : expr => [vars|vars|vars] so that you introduce the variables from the constructors and then the equation.
If you don't give the => ... part, then dummy names are used (since you need to introduce these in order to name hyp).

view this post on Zulip Vincent Siles (Nov 10 2021 at 13:28):

Ok, I'm getting Anomaly "Evar ?X357 was not declared.". I'll try to make a minimal repro see what's happening. Thanks !

view this post on Zulip Notification Bot (Nov 24 2021 at 08:20):

Vincent Siles has marked this topic as resolved.


Last updated: Feb 08 2023 at 08:02 UTC