Struct MutualInductive 

pub struct MutualInductive {
    pub name: String,
    pub sort: Term,
    pub num_params: usize,
    pub constructors: Vec<(String, Term)>,
}

One member of a MUTUAL inductive block: its name, arity sort, uniform parameter count, and constructors (name + full type). Constructor types may reference ANY member of the block — that is the whole point of a mutual declaration.

Fields

name: String

The inductive’s name (e.g. Even).

sort: Term

Its arity sort (e.g. Nat → Prop).

num_params: usize

How many leading arity arguments are uniform parameters (the rest are indices).

constructors: Vec<(String, Term)>

Constructors: (name, full type), types possibly mentioning sibling members.

Trait Implementations

impl Clone for MutualInductive

fn clone(&self) -> MutualInductive

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for MutualInductive

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

Formats the value using the given formatter.