Struct InductiveEnv 

pub struct InductiveEnv { /* private fields */ }

Environment extension for inductive types.

Implementations

impl InductiveEnv

pub fn new() -> Self

Create a new empty inductive environment.

pub fn add(&mut self, ind: InductiveType) -> Result<(), KernelError>

Add an inductive type to the environment.

pub fn get(&self, name: &Name) -> Option<&InductiveType>

Get an inductive type by name.

pub fn is_constructor(&self, name: &Name) -> bool

Check if a name is a constructor.

pub fn get_constructor_parent(&self, name: &Name) -> Option<&Name>

Get the parent type of a constructor.

pub fn is_recursor(&self, name: &Name) -> bool

Check if a name is a recursor.

pub fn get_recursor_parent(&self, name: &Name) -> Option<&Name>

Get the parent type of a recursor.

pub fn register_in_env( &mut self, ind: &InductiveType, env: &mut Environment, ) -> Result<(), KernelError>

Register an InductiveType into an Environment via ConstantInfo.

This is the checked path: the declaration goes through crate::inductive::derive::add_inductive_family, which typechecks the type and constructor telescopes, enforces the universe rule and WHNF-hardened strict positivity, and derives the recursor itself.

Trait Implementations

impl Default for InductiveEnv

fn default() -> Self

Returns the “default value” for a type.