Struct MetaCtx 

pub struct MetaCtx { /* private fields */ }

The metavariable context: fresh-name supply + the substitution being solved.

Implementations

impl MetaCtx

pub fn new() -> Self

pub fn fresh(&mut self) -> Term

A fresh, unsolved metavariable ?n.

pub fn solution(&self, name: &str) -> Option<&Term>

The solution recorded for metavariable name, if any.

pub fn solve(&mut self, name: &str, term: Term)

Directly bind metavariable name := term, WITHOUT normalizing term. Used when the term is already known well-typed and should be kept structured (e.g. a resolved typeclass instance list_inst Nat (mk Nat Zero), which must not be δ-unfolded into its body). The kernel re-checks the assembled term regardless.

Trait Implementations

impl Clone for MetaCtx

fn clone(&self) -> MetaCtx

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for MetaCtx

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

Formats the value using the given formatter.

impl Default for MetaCtx

fn default() -> MetaCtx

Returns the “default value” for a type.