Struct LayeredTypeClassRegistry 

pub struct LayeredTypeClassRegistry { /* private fields */ }

A layered typeclass registry that supports scoped instance introduction.

Useful for local instance declarations inside tactics or proofs.

Implementations

impl LayeredTypeClassRegistry

pub fn new() -> Self

Create a new empty layered registry.

pub fn push_layer(&mut self)

Push a new empty layer.

pub fn pop_layer(&mut self)

Pop the topmost layer.

pub fn add_instance(&mut self, inst: Instance)

Register an instance in the top layer (or global if no layers).

pub fn add_class(&mut self, class: TypeClass)

Register a class in the global registry.

pub fn find_instance(&self, class: &Name, ty: &Expr) -> Option<&Instance>

Find an instance by searching from the top layer to global.

pub fn depth(&self) -> usize

Current number of layers.

pub fn total_instances(&self) -> usize

Total instance count across all layers.

Trait Implementations

impl Debug for LayeredTypeClassRegistry

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for LayeredTypeClassRegistry

fn default() -> LayeredTypeClassRegistry

Returns the “default value” for a type.