Struct TypeEraser 

pub struct TypeEraser { /* private fields */ }

Performs type erasure on kernel expressions.

Implementations

impl TypeEraser

pub fn new() -> Self

Create a type eraser with the default configuration.

pub fn with_config(config: EraseConfig) -> Self

Create a type eraser with a custom configuration.

pub fn erase_sort(&self) -> ErasedExpr

Erase a sort (universe level) — always becomes TypeErased.

pub fn erase_pi(&self) -> ErasedExpr

Erase a Pi-type — types are always erased to TypeErased.

pub fn erase_lam_body(&self, body: ErasedExpr) -> ErasedExpr

Wrap a lambda body in a Lam node (type annotation already dropped).

pub fn erase_app(f: ErasedExpr, arg: ErasedExpr) -> ErasedExpr

Build an erased application from an already-erased function and argument.

pub fn erase_lit(n: u64) -> ErasedExpr

Erase a natural-number literal.

pub fn optimize(&self, expr: ErasedExpr) -> ErasedExpr

Optimise an erased expression by beta-reducing TypeErased applications.

When the function position of an App is TypeErased, the whole application is also TypeErased (the argument is a type). This recursively simplifies the tree.

Trait Implementations

impl Default for TypeEraser

fn default() -> Self

Returns the “default value” for a type.