pub fn derive_recursor(ctx: &Context, ind: &str) -> KernelResult<(Term, Term)>Expand description
Build I_rec’s term and type for the inductive ind. Returns (recursor_type, recursor_term) where recursor_type is exactly infer_type(recursor_term) — so the
type is, by construction, the one the kernel certifies the term against.