Dear Coq community,
I have been trying to write a function in Ltac2 that takes two arguments:
- a constr ‘x’ that can be of any type
- a constr ‘t’ that is a Type
I want this function to give different output if ‘x’ belongs to the Type of ‘t’ than in the case in which it does not.
The following is a minimal example of the best I managed to produce so far.
However, it does not work as intended.
&t does not seem to substitute the value stored in
From Ltac2 Require Import Ltac2. From Ltac2 Require Option. From Ltac2 Require Import Message. Require Import Bool. Ltac2 match_type (x:constr) (t:constr) := match! x with | &t => concat (concat (of_constr x) (of_string " is of type ")) (of_constr t) | _ => concat (concat (of_constr x) (of_string " is not of type ")) (of_constr t) end. Goal True. print (match_type (constr:(2)) (constr:(nat))). print (match_type (constr:(1)) (constr:(bool))).
It produces the following output:
2 is of type nat 1 is of type bool
which is clearly not desirable!
I know there is a function
of type in Ltac1 that would probably make this possible.
However, my question is, is there also a Ltac2-native way to build the function I specified?