Struct RecInfo 

pub struct RecInfo {
    pub all: Rc<[NameId]>,
    pub num_params: u32,
    pub num_indices: u32,
    pub num_motives: u32,
    pub num_minors: u32,
    pub rules: Rc<[RecRule]>,
    pub k: bool,
    pub is_unsafe: bool,
    pub major_induct: NameId,
}

Fields

all: Rc<[NameId]>

num_params: u32

num_indices: u32

num_motives: u32

num_minors: u32

rules: Rc<[RecRule]>

k: bool

is_unsafe: bool

major_induct: NameId

The inductive type of the major premise (for a nested auxiliary recursor this is the nested type, e.g. List).

Implementations

impl RecInfo

pub fn major_idx(&self) -> usize

pub fn first_index_idx(&self) -> usize

Trait Implementations

impl Clone for RecInfo

fn clone(&self) -> RecInfo

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for RecInfo

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

Formats the value using the given formatter.

impl PartialEq for RecInfo

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

Tests for self and other values to be equal, and is used by ==.

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

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for RecInfo