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: Aug 11 2022 at 02:03 UTC