Pierre Vial (Jul 03 2020 at 15:19): Pierre Vial (Jul 03 2020 at 15:19):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...
Théo Winterhalter (Jul 03 2020 at 15:22):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.
Pierre Vial (Jul 03 2020 at 15:28):This works great, thanks again @Théo Winterhalter !
Last updated: Apr 18 2024 at 04:02 UTC