Hi, I was curious if there is a real added value to have `Equations`

and `Equations?`

?

- I know it behaves differently concerning obligations but I am not really sure what would be the advantages of using
`Equations`

and dealing with obligations using`Next Obligation`

rather than the proof mode. - Is there a reason why
`Equations?`

returns a warning if you use it to define a function that do not generate obligations ? It would make sense to me to use`Equations?`

, this way I would see it directly when obligations are left to deal with.

I think it's because `Equations?`

doesn't open proof mode when it doesn't produce any obligation?

I'm also a user of `Equations?`

because VSCoq doesn't support obligations well.

From what I have gathered, it is because you have to open the proof mode before knowing if there are obligations left unsolved or not. But if you can raise a warning if there is none left, I don't see why you couldn't just close the proof mode.

Last updated: Oct 13 2024 at 01:02 UTC