pub fn check_positivity_for_test(
inductive: &str,
constructor: &str,
ty: &Term,
) -> KernelResult<()>Expand description
Strict-positivity check of a constructor type — exposed so tests can pin the paradox fence (negative occurrences rejected, positive functional fields accepted) directly.