Hello, I try to develop a minimal teaching example of `Equations`

where inspect patterns are used. I would like this example to run in an abstract context.

```
From Equations Require Import Equations.
Require Import List.
Inductive hide (P : Prop) := hide_cons : P -> hide P.
Section iterates.
Variable (A : Type) (f : A -> option A) (lt : A -> A -> Prop).
Hypothesis lt_wf : well_founded lt.
(* We don't want this hypothesis to be used automatically by Equations. *)
Hypothesis decr_f : hide (forall n p, f n = Some p -> lt p n ).
Definition f_inspect (n : A) : {p' | f n = p'} :=
exist _ (f n) eq_refl.
Equations f_sequence (n : A) : list A by wf n lt :=
f_sequence n with f_inspect n := {
| exist _ (Some p) eq1 => p :: f_sequence p;
| exist _ None _ => nil
}.
```

But this fails with a message "Unable to satisfy the following constraints: .... ?w : WellFounded ,,,". What should I add to avoid this message? I understand it is a configuration of the type classes mechanism...

You probably need to add

```
Instance WellFounded_lt : WellFounded lt := lt_wf.
```

There is both `well_founded`

(a type scheme) and `WellFounded`

the type class

This topic was moved here from #Coq users > Equations in an abstract setting by Théo Zimmermann

Thx Jakob, this solves my question.

In fact, another solution is to declare the various variables in the following manner.

```
Context {A : Type} (f : A -> option A) {lt : A -> A -> Prop}
`{WellFounded A lt}.
```

Last updated: Jun 14 2024 at 19:02 UTC