Hello!

I'm trying to write directly(*) a reified proof that A -> A, for all type A. The final goal is to verify some type transformations that are not definable in Coq, but I just want to check that I'm able to do so when the transfo is the identity...

In the course of the proof. I'm trying to destruct a sigma type in my goal.

(*): i.e. without using the Template monad.

```
destruct ( ∑ (Sigma : global_env_ext) (Gamma : context) (t0 : term), Sigma;;; Gamma |- t0 : tProd nAnon A A).
```

But Coq is unhappy about that:

```
Error:
Unable to satisfy the following constraints:
In environment:
A : term
Sigma : global_env_ext
Gamma : context
t0 : term
?H : "config.checker_flags"
```

How should I write my destruct with the proper flag? I'm a bit puzzled, because the notation |- seems to take only 4 arguments...

You are missing the` checker_flags`

that tell whether you have `Type : Type`

basically.

I think the easiest would be to write somewhere earlier in your file that you want the defautl.

```
Existing Instance config.default_checker_flags.
```

The file in question is rather readable if you care about the specifics, but I don't think you have to.

This works great, thanks again @Théo Winterhalter !

Last updated: Mar 03 2024 at 16:02 UTC