Class ImplicitHandler

leanr-elab/src/implicit.rs:10–13

Implicit argument handler

/// Implicit argument handler
pub struct ImplicitHandler {
    /// Metavariable context
    mctx: MetaVarContext,
}

impl ImplicitHandler {
    /// Create a new implicit handler