pub fn detect(family_names: &[Name], ty: &Expr) -> Option<NestedOcc>Expand description
Detect a nested occurrence at a strict-positivity leaf.
Given the WHNF of a constructor-field type whose spine is not a direct
application of a family member, return the nested occurrence when the spine
head is a foreign constant (not itself a family member) and at least one
argument mentions a family-being-defined type. Returns None for
- a non-
Consthead (nothing to un-nest here), - a direct occurrence of a family member (
C ∈ family_names— that is ordinary recursion, handled elsewhere), or - a foreign constant none of whose arguments mention the family (a plain
non-recursive field such as
List Nat).
The check is purely syntactic and environment-free so it can be unit-tested in isolation; declaredness and parameter-position validation are deferred to S2.