File inductive.rs

crates/kernel/src/inductive.rs:None–None

//! Inductive type validation and recursor generation.
//!
//! Validates inductive declarations (parameter agreement, positivity, universe
//! constraints, return types) and generates canonical recursors following