Can I make the definition `foo`

in-line in Ltac, i.e, without the auxiliary definition `abstracted`

? I think it relies on a *simultaneous* version of `set`

or `rewrite`

, otherwise things become ill typed (see one example with the aborted `foo'`

definition).

```
Parameter B : bool -> Type.
Parameter C : forall a, B a -> Type.
Parameter f : bool -> bool.
Parameter g : forall a, B a -> B (f a).
Lemma abstracted (fa : bool) (gab : B fa) (c : C fa gab) : Type.
destruct fa. (* arbitrary *)
- exact True.
- exact False.
Defined.
Definition foo a b (c : C (f a) (g a b)) : Type := abstracted (f a) (g a b) c.
Definition foo' a b (c : C (f a) (g a b)) : Type.
set (gab := g a b) in *.
set (fa := f a) in *.
Fail destruct fa.
Abort.
```

Assume I actually want to use `b`

and `c`

in place of `exact True.`

and `exact False.`

.

```
Definition foo' a b (c : C (f a) (g a b)) : Type.
Proof.
revert c. generalize (g a b). destruct (f a).
```

Cheers!

James Wood has marked this topic as resolved.

Last updated: May 24 2024 at 22:02 UTC