`add_inductive` creates only barebones inductive types and no `add_structure` available

[cipher1024]

Prerequisites

• [x] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs, or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

[Description of the issue]

Steps to Reproduce

1. Write the following in a Lean source file:

open tactic
run_cmd do
  let e : expr := expr.const `test [],
  NAT ← mk_const `nat,
  let e := expr.pi `y binder_info.default NAT e,
  let e := expr.pi `x binder_info.default NAT e,
  add_inductive `test [] 0 `(Type) [(`test.mk, e)] ff

inductive test' : Type
| mk : nat -> nat -> test'

#print prefix test'
#print prefix test

Expected behavior: [What you expect to happen]

-- #print prefix test'
-- test' : Type
-- test'.cases_on : Π {C : test' → Sort l} (n : test'), (Π (a a_1 : ℕ), C (test'.mk a a_1)) → C n
-- test'.has_sizeof_inst : has_sizeof test'
-- test'.mk : ℕ → ℕ → test'
-- test'.mk.inj : ∀ {a a_1 a_2 a_3 : ℕ}, test'.mk a a_1 = test'.mk a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- test'.mk.inj_arrow : Π {a a_1 a_2 a_3 : ℕ}, test'.mk a a_1 = test'.mk a_2 a_3 → Π ⦃P : Sort l⦄, (a = a_2 → a_1 = a_3 → P) → P
-- test'.mk.sizeof_spec : ∀ (a a_1 : ℕ), test'.sizeof (test'.mk a a_1) = 1 + sizeof a + sizeof a_1
-- test'.no_confusion : Π {P : Sort l} {v1 v2 : test'}, v1 = v2 → test'.no_confusion_type P v1 v2
-- test'.no_confusion_type : Sort l → test' → test' → Sort l
-- test'.rec : Π {C : test' → Sort l}, (Π (a a_1 : ℕ), C (test'.mk a a_1)) → Π (n : test'), C n
-- test'.rec_on : Π {C : test' → Sort l} (n : test'), (Π (a a_1 : ℕ), C (test'.mk a a_1)) → C n
-- test'.sizeof : test' → ℕ

Actual behavior: [What actually happens]

-- #print prefix test
-- test : Type
-- test.mk : ℕ → ℕ → test
-- test.rec : Π {C : test → Sort l}, (Π (x y : ℕ), C (test.mk x y)) → Π (n : test), C n

Reproduces how often: [What percentage of the time does it reproduce?] 100%

Versions

Lean (version 3.3.1, commit 5efa1b829cfb, RELEASE)

Additional Information

Also, no add_structure function is available to enable structure syntax such as { foo with field := new }.