I notice that tmLemma
tmDefinition
, and tmAxiomRed
all returns the defined constant which makes it easier to manipulate the generated term, however the same is not true to tmMkInductive
. What's the reason for this? And is there an easy way to retrieve it?
I've been banging my head against this issue for a while now and the only solution I could find for now is to break the program in two runs and provide the defined constant on the second one, which is annoying.
I guess tmMkInductive
introduce multiple new constants (for the type, its constructors, and possibly also the generated eliminators) and not a single one. Couldn't you tmUnquote
what you need just after making the inductive ?
That's what I was doing, but then I need to manipulate terms of that type later in the monad and I can't destruct them, would you have a suggestion how to deal with that?
I think I would have the same issue with tmDefinition
and alike though, I can't run the function that was just defined, can I?
I think I'm having difficulty to find what exactly should I tmUnquote
in this case. For example, assume we have
MetaCoq Run (
t <- tmLocate1 "bool";;
tbool <- match t with
| IndRef ind => ...?
| _ => tmFail "not IndRef"
end
).
What should I unquote here to have the type constructor bool
at hand?
I tried to QuoteConstant
the inductive_mind
but I get an error
MetaCoq Run (
t <- tmLocate1 "bool";;
mind <- match t with
| IndRef {| inductive_mind := mind |} =>
tmReturn mind
| _ => tmFail "not Const"
end ;;
t <- tmQuoteConstant mind false).
Error: Anomaly "File "clib/int.ml", line 46, characters 14-20: Assertion failed."
Please report at http://coq.inria.fr/bugs/.
And if I do QuoteInductive
I don't seem to find what exactly should I get from the mutual_inductive_body
. Sorry if I'm missing something obvious.
Your "t" is already the global reference corrsponding to bool, and mind
its representation. You can then either use mib <- tmQuoteInductive mind
which gives you the mutual inductive declaration, and then nth_error (mib.(ind_bodies)) 0
will be the first (and only) inductive declaration, or just use tInd mind []
to refer to bool
in a term.
Also, tConstruct mind 0 []
will refer to the first bool
constructor
Last updated: Feb 09 2023 at 02:02 UTC