Method check_nested_ctor_fields_loop

crates/kernel/src/inductive.rs:1898–1915

Walk the remaining forall binders of a nested constructor type and check each field domain for positivity against the augmented address set.

(
    &mut self,
    ty: &KExpr<M>,
    augmented_addrs: &[Address],
  )

                  return Err(TcError::Other(
                    "positivity: nested ctor not found".into(),
                  ));
                },
              };
              self.check_nested_ctor_fields(
                &ctor_ty,
                n_params,
                &param_args,
                &us,
                &augmented,
              )?;
            }

            Ok(())
          },
          _ => {
            Err(TcError::Other("positivity: not a valid inductive app".into()))
          },
        }
      },
    }
  }