Hello,

Is there anyway to suppress warnings emitted by Equations (such as "Functional induction principle could not be proved automatically" for instance) by any chance?

I'm aware of the `Set Warnings "-flag"`

to silence warnings identified by `flag`

, but it doesn't seem to support plugins's warnings?

looks like equations is not using the warning control system (at least for this warning)

you can report an issue on the equations repo

Reported, thanks for the prompt answer Gaëtan!

I think the better solution here is to tell Equations not to try and derive the induction principle? Using

```
#[derive(eliminator=no)]Equations …
```

or even

```
#[derive(equations=no)]Equations …
```

if you also do not want to generate the unfolding equations

Shouldn't Equations always succeed in deriving the induction principle ?

As far as I understand, if the definitions use tricky dependent pattern-matching, deriving the unfolding equations can be tricky, especially in the absence of funext, and the induction principle depends on them. I don't know if there are other sources of incompleteness, but in the end Equations is a best-effort, and there are horrible corner-cases where it chokes.

But are those cases bugs/implementation restrictions, or is there a more fundamental reason?

Meven Lennon-Bertrand said:

I think the better solution here is to tell Equations not to try and derive the induction principle? Using

`#[derive(eliminator=no)]Equations …`

or even

`#[derive(equations=no)]Equations …`

if you also do not want to generate the unfolding equations

That's useful in a few cases, thanks! Unfortunately, I have cases where `derive (eliminator=no)`

prevents the derivation of `*_graph_correct`

which breaks proofs later on.

Note that it seems to be interaction with `SProp`

mostly that messes up things for Equations

Hopefully, things will be smoother there once we have sort polymorphism

Last updated: Oct 13 2024 at 01:02 UTC