pub trait Table {
type Sort: Sort;
type Term: Term<Type = Self::Var>;
type Theorem: Theorem;
type Var: Var;
// Required methods
fn sort(&self, idx: u8) -> Option<&Self::Sort>;
fn nr_sorts(&self) -> u8;
fn term(&self, idx: u32) -> Option<&Self::Term>;
fn nr_terms(&self) -> u32;
fn theorem(&self, idx: u32) -> Option<&Self::Theorem>;
fn nr_theorems(&self) -> u32;
fn unify_commands(&self, idx: Range<usize>) -> Option<&[Command<Unify>]>;
fn unify_command(&self, idx: usize) -> Option<&Command<Unify>>;
fn binders(&self, idx: Range<usize>) -> Option<&[Self::Var]>;
}Expand description
An interface that enables queries for properties of sorts, terms and theorems.
Required Associated Types§
type Sort: Sort
type Term: Term<Type = Self::Var>
type Theorem: Theorem
type Var: Var
Required Methods§
fn sort(&self, idx: u8) -> Option<&Self::Sort>
fn nr_sorts(&self) -> u8
fn term(&self, idx: u32) -> Option<&Self::Term>
fn nr_terms(&self) -> u32
fn theorem(&self, idx: u32) -> Option<&Self::Theorem>
fn nr_theorems(&self) -> u32
fn unify_commands(&self, idx: Range<usize>) -> Option<&[Command<Unify>]>
fn unify_command(&self, idx: usize) -> Option<&Command<Unify>>
fn binders(&self, idx: Range<usize>) -> Option<&[Self::Var]>
Dyn Compatibility§
This trait is dyn compatible.
In older versions of Rust, dyn compatibility was called "object safety".