Struct InductiveSpec 

pub struct InductiveSpec {
    pub name: Name,
    pub ty: Expr,
    pub ctors: Vec<(Name, Expr)>,
    pub rec_name: Option<Name>,
}

A single inductive type inside a (possibly mutual) family declaration.

Fields

name: Name

Name of the inductive type.

ty: Expr

Full type: Π params.. indices.., Sort l.

ctors: Vec<(Name, Expr)>

Constructors as (name, full type) pairs. The constructor type must re-bind the family parameters first.

rec_name: Option<Name>

Optional explicit recursor name (defaults to <name>.rec).

Implementations

impl InductiveSpec

pub fn new(name: Name, ty: Expr, ctors: Vec<(Name, Expr)>) -> Self

Create a spec with the default recursor name <name>.rec.

pub fn with_rec_name(self, rec_name: Name) -> Self

Override the generated recursor’s name.

Trait Implementations

impl Clone for InductiveSpec

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 InductiveSpec

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

Formats the value using the given formatter.