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 installed::add_derived_family;

pub use installed::escaped_name;

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 supplied::same_up_to_binders;

pub use supplied::supplied_type_matches;

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

installed

The guard of an install: every constant that a term the kernel derived names resolves, and to the constant the derivation meant.

labelset_traits

LabelSet - Trait Implementations

nested

Nested-to-mutual inductive elaboration (C10).

smallmap_traits

SmallMap - Trait Implementations

statsummary_traits

StatSummary - Trait Implementations

supplied

A term that arrives from outside, held against the term the kernel made.

transformstat_traits

TransformStat - Trait Implementations

types

Auto-generated module

windowiterator_traits

WindowIterator - Trait Implementations