[−][src]Struct nar::check::monad::meta::MetaContext
Methods
impl<Val> MetaContext<Val>[src]
pub fn solutions(&self) -> &Vec<MetaSol<Val>>[src]
pub fn solution(&self, index: MI) -> &MetaSol<Val>[src]
pub fn mut_solutions(&mut self) -> &mut Vec<MetaSol<Val>>[src]
pub fn expand_with_fresh_meta(&mut self, meta_count: MI)[src]
Add many unsolved metas to the context.
pub fn fresh_meta(&mut self, new_meta: impl FnOnce(MI) -> Val) -> Val[src]
Create a new valid but unsolved meta variable, used for generating fresh metas during elaboration.
impl<Val: Debug + Eq> MetaContext<Val>[src]
pub fn solve_meta(&mut self, meta_index: MI, at: DBI, solution: Val)[src]
Submit a solution to a meta variable to the context.
Trait Implementations
impl<Val: Clone> Clone for MetaContext<Val>[src]
fn clone(&self) -> MetaContext<Val>[src]
fn clone_from(&mut self, source: &Self)1.0.0[src]
impl<Val: Debug> Debug for MetaContext<Val>[src]
impl<Val> Default for MetaContext<Val>[src]
impl<Val: Display> Display for MetaContext<Val>[src]
Auto Trait Implementations
impl<Val> RefUnwindSafe for MetaContext<Val> where
Val: RefUnwindSafe,
Val: RefUnwindSafe,
impl<Val> Send for MetaContext<Val> where
Val: Send,
Val: Send,
impl<Val> Sync for MetaContext<Val> where
Val: Sync,
Val: Sync,
impl<Val> Unpin for MetaContext<Val>
impl<Val> UnwindSafe for MetaContext<Val> where
Val: UnwindSafe,
Val: UnwindSafe,
Blanket Implementations
impl<T> Any for T where
T: 'static + ?Sized, [src]
T: 'static + ?Sized,
impl<T> Borrow<T> for T where
T: ?Sized, [src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized, [src]
T: ?Sized,
fn borrow_mut(&mut self) -> &mut T[src]
impl<T> From<T> for T[src]
impl<T, U> Into<U> for T where
U: From<T>, [src]
U: From<T>,
impl<T> ToOwned for T where
T: Clone, [src]
T: Clone,
type Owned = T
The resulting type after obtaining ownership.
fn to_owned(&self) -> T[src]
fn clone_into(&self, target: &mut T)[src]
impl<T> ToString for T where
T: Display + ?Sized, [src]
T: Display + ?Sized,
impl<T, U> TryFrom<U> for T where
U: Into<T>, [src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>, [src]
U: TryFrom<T>,