Struct InductiveTypeBuilder 

pub struct InductiveTypeBuilder { /* private fields */ }

Builder for constructing InductiveType declarations incrementally.

Implementations

impl InductiveTypeBuilder

pub fn new() -> Self

Create an empty builder.

pub fn name(self, name: Name) -> Self

Set the inductive type name.

pub fn univ_params(self, params: Vec<Name>) -> Self

Set universe parameters.

pub fn num_params(self, n: u32) -> Self

Set number of type parameters.

pub fn num_indices(self, n: u32) -> Self

Set number of type indices.

pub fn ty(self, ty: Expr) -> Self

Set the sort of the inductive type.

pub fn intro_rule(self, name: Name, ty: Expr) -> Self

Add a constructor/introduction rule.

pub fn is_prop(self, v: bool) -> Self

Mark as a Prop-valued inductive type (proof-irrelevant).

pub fn is_nested(self, v: bool) -> Self

Mark as a nested inductive type.

pub fn build(self) -> Result<InductiveType, String>

Build the InductiveType. Returns Err if name or ty is missing.

Trait Implementations

impl Default for InductiveTypeBuilder

fn default() -> Self

Returns the “default value” for a type.