Quote and unquote a list

quote.v

Require Import MetaCoq.Template.Loader.

Quote Recursively Definition list_syntax := 
ltac:(let t := eval compute in list in exact t).

Make Definition list_from_syntax :=
  ltac:(let t := eval cbv in list_syntax in exact t).

(*
Error:
inspect_term: cannot recognize ([InductiveDecl
                                   "Coq.Init.Datatypes.list"%string
                                   {|
                                   ind_finite := Finite;
                                   ind_npars := 1;
                                   ind_params := [{|
                                           decl_name := nNamed
                                           "A"%string;
                                           decl_body := None;
                                           decl_type := tSort
                                           (utils.NEL.sing
                                           (
                                           Level.Level
                                           "Coq.Init.Datatypes.44",
                                           false)) |}];
                                   ind_bodies := [{|
                                           ind_name := "list"%string;
                                           ind_type := tProd
                                           (nNamed "A"%string)
                                           (tSort
                                           (utils.NEL.sing
                                           (
                                           Level.Level
                                           "Coq.Init.Datatypes.44",
                                           false)))
                                           (tSort
                                           (utils.NEL.cons
                                           (Level.lSet, false)
                                           (utils.NEL.sing
                                           (
                                           Level.Level
                                           "Coq.Init.Datatypes.44",
                                           false))));
                                           ind_kelim := [InProp;
                                           InSet; InType];
                                           ind_ctors := [
                                           ("nil"%string,
                                           tProd
                                           (nNamed "A"%string)
                                           (tSort
                                           (utils.NEL.sing
                                           (
                                           Level.Level
                                           "Coq.Init.Datatypes.44",
                                           false)))
                                           (tApp (tRel 1) [tRel 0]),
                                           0);
                                           ("cons"%string,
                                           tProd
                                           (nNamed "A"%string)
                                           (tSort
                                           (utils.NEL.sing
                                           (
                                           Level.Level
                                           "Coq.Init.Datatypes.44",
                                           false)))
                                           (tProd nAnon 
                                           (tRel 0)
                                           (tProd nAnon
                                           (tApp (tRel 2) [tRel 1])
                                           (tApp (tRel 3) [tRel 2]))),
                                           2)];
                                           ind_projs := [] |}];
                                   ind_universes := Monomorphic_ctx
                                           (
                                           {|
                                           LevelSet.this := [Level.Level
                                           "Coq.Init.Datatypes.44"];
                                           LevelSet.is_ok := LevelSet.Raw.add_ok
                                           (s:=[])
                                           (Level.Level
                                           "Coq.Init.Datatypes.44")
                                           LevelSet.Raw.empty_ok |},
                                           {|
                                           ConstraintSet.this := [];
                                           ConstraintSet.is_ok := ConstraintSet.Raw.empty_ok |}) |}],
                               tInd
                                 {|
                                 inductive_mind := "Coq.Init.Datatypes.list";
                                 inductive_ind := 0 |} []) (maybe you forgot to reduce it?)
*)