fix(library/init/meta/expr,library/vm/vm_expr): fix macro args

library/init/meta/expr.lean

@@ -334,7 +334,7 @@ private meta def macro_args_to_list_aux (n : nat) (args : fin n → expr) : Π (
 | (i+1) h := args ⟨i, h⟩ :: macro_args_to_list_aux i (nat.le_trans (nat.le_succ _) h)
 
 meta def macro_args_to_list (n : nat) (args : fin n → expr) : list expr :=
-macro_args_to_list_aux n args n (nat.le_refl _)
+(macro_args_to_list_aux n args n (nat.le_refl _)).reverse
 
 meta def to_raw_fmt : expr → format
 | (var n) := p ["var", to_fmt n]

src/library/vm/vm_expr.cpp

@@ -204,7 +204,7 @@ unsigned expr_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
         break;
     case expr_kind::Macro:
         data.push_back(to_obj(macro_def(e)));
-        data.push_back(to_obj(macro_num_args(e)));
+        data.push_back(mk_vm_nat(macro_num_args(e)));
         data.push_back(mk_vm_closure(g_expr_macro_arg_fun_idx, 1, &o));
         break;
     }

tests/lean/macro_args.lean

@@ -0,0 +1 @@
+#eval ``({pos . line := zero, col := 1}).to_raw_expr.to_raw_fmt

tests/lean/macro_args.lean.expected.out

@@ -0,0 +1 @@
+[macro structure instance (const zero []) [macro prenum]]