I could write a list filtering function with `Equations`

plugin like

this:

```
Equations filter_tru {A: Type} (f: A -> bool) (l: list A): list A :=
filter_tru f [] := [];
filter_tru f (x::l) with f x => {
| true => x :: (filter_tru f l)
| false => filter_tru f l
}.
```

Is there some provision to 'share' the `f`

argument?

Something like this?

```
Equations filter_tru {A: Type} (f: A -> bool) (l: list A): list A :=
filter_tru f => {
| [] => []
| x::l' with f x => {
| true => x :: (filter_tru f x)
| false => filter_tru f x
}
}.
(*
Syntax error: ''' or [term level 99] expected after '{' (in [term]).
*)
```

Yes you can and you already use the syntax to match on `f x`

:

```
Equations filter_tru {A : Type} (f : A -> bool) (l : list A) : list A :=
filter_tru f ll with ll => {
| [] => []
| x :: l with f x => {
| true => x :: filter_tru f l
| false => filter_tru f l
}
}.
```

Note that I had to give a different name to `ll`

and `l`

because Equations doesn't let you shadow a variable.

Note that you also don't have to repeat the name of the function as the following is also accepted:

```
Equations filter_tru {A : Type} (f : A -> bool) (l : list A) : list A :=
| f, [] => []
| f, x :: l with f x => {
| true => x :: filter_tru f l
| false => filter_tru f l
}.
```

You can combine it all to get this:

```
Equations filter_tru {A : Type} (f : A -> bool) (l : list A) : list A :=
| f, ll with ll => {
| [] => []
| x :: l with f x => {
| true => x :: filter_tru f l
| false => filter_tru f l
}
}.
```

This topic was moved here from #Coq users > Equations: Common arguments by Karl Palmskog.

Last updated: Oct 13 2024 at 01:02 UTC