@Thomas Lamiaux in section 2 in your tutorial of *Equations Basics*, you briefly mention a case where you can use `{ }`

within a `with`

clause to discard an impossible case. Where does this notation come from ? Only importing Equations doesn't bring it up. Also, can it only be used with `with`

clauses?

It is just the usual with notation but as you do it on False it has no branches

Nothing fancy there I think

Thomas Lamiaux said:

It is just the usual with notation but as you do it on False it has no branches

What does the `{ }`

notation expand to? False? How can I signal to Equations to create a new obligation to prove a certain branch isn't possible?

Last updated: Oct 13 2024 at 01:02 UTC