Struct RecursorVal 

pub struct RecursorVal {
    pub common: ConstantVal,
    pub all: Vec<Name>,
    pub num_params: u32,
    pub num_indices: u32,
    pub num_motives: u32,
    pub num_minors: u32,
    pub rules: Vec<RecursorRule>,
    pub k: bool,
    pub is_unsafe: bool,
}

Recursor (eliminator) declaration value.

Fields

common: ConstantVal

Common fields.

all: Vec<Name>

All inductive types in mutual declaration.

num_params: u32

Number of parameters.

num_indices: u32

Number of indices.

num_motives: u32

Number of motive arguments.

num_minors: u32

Number of minor premises (one per constructor).

rules: Vec<RecursorRule>

Reduction rules (one per constructor).

k: bool

Whether this supports K-like reduction.

is_unsafe: bool

Whether this is unsafe.

Implementations

impl RecursorVal

pub fn get_major_idx(&self) -> u32

Get the index of the major premise in the recursor’s arguments.

The major premise is the argument being eliminated. Position: nparams + nmotives + nminors + nindices

pub fn get_first_index_idx(&self) -> u32

Get the total number of arguments before the major premise.

pub fn get_rule(&self, ctor: &Name) -> Option<&RecursorRule>

Find the reduction rule for a given constructor.

Trait Implementations

impl Clone for RecursorVal

fn clone(&self) -> RecursorVal

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for RecursorVal

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

Formats the value using the given formatter.

impl PartialEq for RecursorVal

fn eq(&self, other: &RecursorVal) -> 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 RecursorVal