Module functions 

Auto-generated module

🤖 Generated with SplitRS

Functions

check_inductive

Check an inductive type declaration for validity.

constructor_field_counts

Given an InductiveType, return the number of fields in each constructor.

is_enum_inductive

Check whether an inductive type is an enum (all constructors have no fields).

is_singleton_inductive

Check whether an inductive type is a singleton (one constructor, no recursive fields).

mk_bool_inductive

Build the Bool inductive type (no parameters, two constructors).

mk_empty_inductive

Build the Empty inductive type (no constructors — ex falso).

mk_nat_inductive

Build the Nat inductive type.

mk_unit_inductive

Build the Unit inductive type (single constructor, no fields).

recursor_name

Return the recursor name for a given inductive type name.

reduce_recursor

Reduce a recursor application (iota-reduction).