Struct NestedOcc 

pub struct NestedOcc {
    pub container: Name,
    pub container_levels: Vec<Level>,
    pub args: Vec<Expr>,
    pub family_positions: Vec<usize>,
}

A nested occurrence C Ds Is: a family-being-defined type appears inside the arguments of an already-declared foreign inductive C.

This is the raw syntactic capture produced at a strict-positivity leaf. It does not yet decide whether C is a declared inductive, nor whether the family occurs in a legal parameter position versus an (unsupported) index position — that validation happens in S2 against C’s InductiveVal.

Fields

container: Name

The foreign container inductive C (e.g. List, Array).

container_levels: Vec<Level>

C’s universe-level arguments.

args: Vec<Expr>

The full argument spine Ds ++ Is of the container application, in source order.

family_positions: Vec<usize>

Indices into args whose term mentions a family-being-defined type. In Array Syntax this is [0]; these are the positions S2 abstracts into fresh leading parameters (after checking they are parameter, not index, positions of C).

Trait Implementations

impl Clone for NestedOcc

fn clone(&self) -> Self

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for NestedOcc

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Eq for NestedOcc

impl PartialEq for NestedOcc

fn eq(&self, other: &Self) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl StructuralPartialEq for NestedOcc