Does Equations support simultaneous `with`

-abstraction, and in particular the `inspect`

idiom?

This topic was moved here from #Coq users > Equations simultaneous `with`

by Karl Palmskog.

I think the inspect idiom appears in examples, even by name

OTOH, I can't find examples with multiple `with`

clauses :-|... the grammar in the manual might suggest that `|`

works?

No sorry, it should be `,`

, see the last line:

image.png

The example doesn't abstract over the thing being inspected (the Agda docs explain this fairly well), but I'll give comma a go. Thanks!

The only example I know uses multiple with clauses (in this file from metacoq)

So, as far as I can tell, having multiple `with`

-expressions just does a sequence of `with`

-abstractions, rather than one simultaneous `with`

-abstraction. Adapting example `f₃`

from the Agda docs produces an ill typed term:

```
From Equations Require Import Equations.
Axiom T : nat -> Set.
Axiom H : forall x y, T (x + y) -> Set.
Equations? f3 : forall x y (t : T (x + y)) (h : H x y t), T (x + y) :=
| x, y, t, h with h, x + y => {
| w2, w1 => _
}.
```

However, this seems to be good enough for the (full) inspect idiom, or at least my use case.

Hmm, maybe it's not enough for my next use case. Is there any way to do a simultaneous `with`

-abstraction in Ltac?

Last updated: Oct 13 2024 at 01:02 UTC