pub fn check_positivity_mutual(
block: &[&str],
constructor: &str,
ty: &Term,
) -> KernelResult<()>Expand description
Check strict positivity of a MUTUAL BLOCK of inductives in a constructor type.
A constructor of one block member may recursively reference ANY member — Even’s
even_succ : Π(n). Odd n → Even (Succ n) places the sibling Odd in a
strictly-positive recursive position. The block is treated as a single “inductive”
for positivity: an occurrence of any member to the RIGHT of every arrow is a
(recursive) occurrence and allowed; any member in a DOMAIN is a negative
occurrence and rejected — so a cross-block paradox (Even n → False) → Odd n is
caught exactly as a self-negative one is.