pub fn register_inductive(env: &mut Env, decl: InductiveDecl)Expand description
Install an inductive declaration on the environment: register the type,
every constructor, and the generated eliminator together with its
dependent Pi-type. Mirrors registerInductive in the JavaScript kernel.