Stream: MetaCoq

Topic: tmUnquoteTyped


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

view this post on Zulip Théo Winterhalter (Jun 10 2020 at 08:40):

tmUnQuoteTyped is part of the monad, and can only be executed with Run TemplateProgram.

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

view this post on Zulip Théo Winterhalter (Jun 10 2020 at 08:42):

If you now run

Run TemplateProgram unquoteT_reif_true.

it should end in an error.

view this post on Zulip Pierre Vial (Jun 10 2020 at 08:43):

Indeed, thanks!!


Last updated: Aug 11 2022 at 02:03 UTC