pub fn check_positivity_mutual_resolved(
ctx: &Context,
block: &[&str],
constructor: &str,
ty: &Term,
) -> KernelResult<()>Expand description
check_positivity_resolved for a MUTUAL block — the same δ resolution, and a member
hidden behind an alias is a member of the block for every question asked here.