Module inductive 

Auto-generated module structure

Re-exports

pub use derive::add_inductive_family;

pub use derive::check_and_derive_family;

pub use derive::derive_family_unchecked;

pub use derive::DerivedFamily;

pub use derive::InductiveSpec;

pub use nested::check_and_derive_family_nested;

pub use nested::detect as detect_nested;

pub use nested::restore as restore_nested;

pub use nested::specialize as specialize_nested;

pub use nested::verify_nested_bundle;

pub use nested::AuxMap;

pub use nested::ExpandedFamily;

pub use nested::NestedOcc;

pub use focusstack_traits::*;

pub use functions::*;

pub use inductiveenv_traits::*;

pub use inductiveerror_traits::*;

pub use inductivetypebuilder_traits::*;

pub use labelset_traits::*;

pub use smallmap_traits::*;

pub use statsummary_traits::*;

pub use transformstat_traits::*;

pub use types::*;

pub use windowiterator_traits::*;

Modules

derive

Kernel-side inductive family checking and recursor derivation.

focusstack_traits

FocusStack - Trait Implementations

functions

Auto-generated module

inductiveenv_traits

InductiveEnv - Trait Implementations

inductiveerror_traits

InductiveError - Trait Implementations

inductivetypebuilder_traits

InductiveTypeBuilder - Trait Implementations

labelset_traits

LabelSet - Trait Implementations

nested

Nested-to-mutual inductive elaboration (C10).

smallmap_traits

SmallMap - Trait Implementations

statsummary_traits

StatSummary - Trait Implementations

transformstat_traits

TransformStat - Trait Implementations

types

Auto-generated module

windowiterator_traits

WindowIterator - Trait Implementations