I'm trying to build myself the reification of the formula "2 = 1" using the reifications of
nat, but I fail, seemingly because I cannot remove some tEvar which appear in the reification of =. Things work fine if I reify
eq nat instead of just
eq, but I would like to proceed generically. How should I do to discard tEvar while reifying
From MetaCoq Require Import All. Require Import MetaCoq.Template.All. Require Import List String. Import ListNotations MonadNotation. MetaCoq Quote Definition zero_reif := 0. MetaCoq Quote Definition one_reif := 1. MetaCoq Quote Definition two_reif := 2. MetaCoq Unquote Definition two_unreif := two_reif. (*everything is fine *) MetaCoq Quote Definition nat_reif := nat. MetaCoq Quote Definition eq_reif_generic := Eval cbn in eq. Print eq_reif_generic. (* tEvar appears in the term *) MetaCoq Quote Definition eq_nat_reif := Eval cbn in (eq nat). Print eq_nat_reif. (* no tEvar *) (** Reification of 2 = 1**) MetaCoq Quote Definition two_equal_one_reif := Eval cbn in (eq 2 1). Print two_equal_one_reif. (** trying to build by myselft the reification of "2 = 1" **) Fail MetaCoq Unquote Definition try2 := (tApp eq_reif_generic [nat_reif; two_reif]). (* The command has indeed failed with message: inspect_term: cannot recognize (tEvar 26 ) (maybe you forgot to reduce it?) *) Fail MetaCoq Unquote Definition try2 := (tApp eq_reif_generic [nat_reif; two_reif ; one_reif ]). (* same fail*) Fail MetaCoq Unquote Definition try3 := (tApp eq_reif_generic [two_reif ; one_reif ]). (* same fail *)
I guess one should call the type checker (type inference actually) on the term in order to infer the evar number 26 must be
Is there an API to call type inference on the unquoted term? Or, is there a type inference algorithm written at the meta level?
(@Pierre Vial I'm not an metacoq expert, I'm just curious)
@Enrico Tassi In the end of Section 2.1 of the MetaCoq project file, it is said that
tEvar is not handled yet. Although it dates back to an older version of MetaCoq, I was hoping that there would be a hack to avoid having
tEvar popping up
Well, actually, reifying
@eq instead of
eq does the job (should have thought of it myself rightaway), but I would still be interested to know if one may call type inference
Right now, we cannot call the inference algorithm of Coq no.
@eq is indeed the _official_ way to go. Generally speaking we do not handle evars yet.
Last updated: Feb 09 2023 at 03:06 UTC