## Stream: Equations devs & users

### Topic: Equations simultaneous `with`

#### James Wood (Feb 28 2022 at 16:57):

Does Equations support simultaneous `with`-abstraction, and in particular the `inspect` idiom?

#### Notification Bot (Feb 28 2022 at 16:59):

This topic was moved here from #Coq users > Equations simultaneous `with` by Karl Palmskog.

#### Paolo Giarrusso (Feb 28 2022 at 18:10):

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

#### Paolo Giarrusso (Feb 28 2022 at 18:14):

OTOH, I can't find examples with multiple `with` clauses :-|... the grammar in the manual might suggest that `|` works?

#### Paolo Giarrusso (Feb 28 2022 at 18:15):

No sorry, it should be `,` , see the last line:
image.png

#### James Wood (Feb 28 2022 at 20:38):

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!

#### Kenji Maillard (Feb 28 2022 at 21:11):

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

#### James Wood (Mar 02 2022 at 10:52):

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 => _
}.
``````

#### James Wood (Mar 02 2022 at 10:52):

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

#### James Wood (Mar 02 2022 at 14:22):

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: Jan 29 2023 at 15:02 UTC