You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Declaring an inductive (tmMkInductive) and unquoting it (tmUnquote) in the same metacoq command unpredictably fails,
depending on which functions are inlined (see MWE).
Here is a MWE to reproduce the bug (I declare a (trivial) inductive and immediately try to unquote it) :
From MetaCoq.Utils RequireImport utils.
From MetaCoq.Template RequireImportAll.
Import MCMonadNotation.
(* Modify this based on the current file. *)Definition ind : term :=
tInd {| inductive_mind := (MPfile ["Bug2"], "Ind") ; inductive_ind := 0 |} [].
(* The simplest inductive you can make. *)Definition mind_body := {|
ind_finite := Finite;
ind_npars := 0;
ind_params := [];
ind_bodies := [{|
ind_name := "Ind";
ind_indices := [];
ind_sort := sProp;
ind_type := tSort sProp;
ind_kelim := IntoPropSProp;
ind_ctors :=[];
ind_projs := [];
ind_relevance := Relevant
|}];
ind_universes := Monomorphic_ctx;
ind_variance := None
|}.
Definition define_ind : TemplateMonad unit :=
tmMkInductive' mind_body.
Definition unquote_ind : TemplateMonad unit :=
tmUnquote ind ;; ret tt.
(* Anomaly : "Inductive Bug2.Ind does not appear in the environment." *)
MetaCoq Run (define_ind ;; unquote_ind).
(* Succeeds. *)
MetaCoq Run define_ind.
MetaCoq Run unquote_ind.
(* Succeeds. *)
MetaCoq Run (tmMkInductive' mind_body ;; unquote_ind).
The text was updated successfully, but these errors were encountered:
Declaring an inductive (
tmMkInductive
) and unquoting it (tmUnquote
) in the same metacoq command unpredictably fails,depending on which functions are inlined (see MWE).
Here is a MWE to reproduce the bug (I declare a (trivial) inductive and immediately try to unquote it) :
The text was updated successfully, but these errors were encountered: