pub fn register_coinductive(env: &mut Env, decl: CoinductiveDecl)Expand description
Install a coinductive declaration on the environment: register the type,
every constructor, and the generated corecursor together with its
dependent Pi-type. Mirrors registerCoinductive in the JavaScript kernel.