Stream: MetaCoq

Topic: Flag for typing judgments


view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Théo Winterhalter (Jul 03 2020 at 15:24):

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

view this post on Zulip Pierre Vial (Jul 03 2020 at 15:28):

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


Last updated: Aug 11 2022 at 02:03 UTC