Pierre Vial (Jun 10 2020 at 08:33): Pierre Vial (Jun 10 2020 at 08:33):Hello,
According to the MetaCoq Project file, "tmUnquoteTyped A tm returns the term whose syntax is tm and checks that it is indeed of type A".
I'm thus perplexed by the following example, which does not show a change of behavior when A is Prop and tm is either the reification of True (Prop) or true (bool). What is it that I'm not getting right?
Quote Definition reif_True := Eval compute in True.
Quote Definition reif_true := Eval compute in true.
Definition unquoteT_reif_True := tmUnquoteTyped Prop reif_True.
Compute unquoteT_reif_True.
Print unquoteT_reif_True.
Definition unquoteT_reif_true := tmUnquoteTyped Prop reif_true.
Compute unquoteT_reif_true.
Print unquoteT_reif_true.
I get in the output:
= tmUnquoteTyped Prop
(tInd
{| inductive_mind := "Coq.Init.Logic.True"; inductive_ind := 0 |}
[])
: TemplateMonad Prop
unquoteT_reif_True = tmUnquoteTyped Prop reif_True
: TemplateMonad Prop
= tmUnquoteTyped Prop
(tConstruct
{|
inductive_mind := "Coq.Init.Datatypes.bool";
inductive_ind := 0 |} 0 [])
: TemplateMonad Prop
unquoteT_reif_true = tmUnquoteTyped Prop reif_true
: TemplateMonad Prop
Where does it tell me that true does not have type Prop ?
Théo Winterhalter (Jun 10 2020 at 08:40):tmUnQuoteTyped is part of the monad, and can only be executed with Run TemplateProgram.
Théo Winterhalter (Jun 10 2020 at 08:41):tmUnquoteTyped Prop reif_true is well-typed, it represents the computation of unquoting reif_true and then checking it has type Prop.
Théo Winterhalter (Jun 10 2020 at 08:42):If you now run
Run TemplateProgram unquoteT_reif_true.
it should end in an error.
Pierre Vial (Jun 10 2020 at 08:43):Indeed, thanks!!
Last updated: Jun 01 2023 at 12:01 UTC