Hi ! I'm testing `Equations`

and have a noob questions:

```
From Equations Require Import Equations.
From Coq Require Import List.
Import ListNotations.
(* Cannot guess decreasing argument of fix *)
Equations f {A: Type} (a: A) (l:list A) : list A :=
f a [] := [] ;
f a [x] := [x];
f a (hd :: tl) := hd :: a :: f a tl
.
```

How to specify the decreasing argument ?

You can add an annotation after the type:

```
Equations f {A: Type} (a: A) (l:list A) : list A by struct l :=
```

But here equations still complains that the recursion does not happen on the right subterm. You can solve it by making more explicit the structure of pattern-matches:

```
Equations f {A: Type} (a: A) (l:list A) : list A:=
f a [] := [] ;
f a (hd :: tl) with tl => {
| [] := [hd] ;
| _ := hd :: a :: f a tl
}.
```

Perfect, thank you @Kenji Maillard

Last updated: May 28 2023 at 18:29 UTC