pub trait CoreVisit<L: Language> {
// Required methods
fn free_variables(&self) -> Vec<CoreVariable<L>>;
fn size(&self) -> usize;
fn assert_valid(&self);
// Provided method
fn references_only_universal_variables(&self) -> bool { ... }
}Required Methods§
Sourcefn free_variables(&self) -> Vec<CoreVariable<L>>
fn free_variables(&self) -> Vec<CoreVariable<L>>
Extract the list of free variables (for the purposes of this function, defined by Variable::is_free).
The list may contain duplicates and must be in a determinstic order (though the order itself isn’t important).
Sourcefn size(&self) -> usize
fn size(&self) -> usize
Measures the overall size of the term by counting constructors etc. Used to determine overflow.
Sourcefn assert_valid(&self)
fn assert_valid(&self)
Asserts various validity constraints and panics if they are not held. These validition constraints should never fail unless there is a bug in our logic. This is to aid with fuzzing and bug detection.
Provided Methods§
Sourcefn references_only_universal_variables(&self) -> bool
fn references_only_universal_variables(&self) -> bool
True if this term references only universal variables. This means that it contains no existential variables. If this is a goal, then when we prove it true, we don’t expect any substitution. This is similar, but not identical, to the commonly used term “ground term”, which in Prolog refers to a term that contains no variables. The difference here is that the term may contain variables, but only those instantiated universally (∀).
Dyn Compatibility§
This trait is dyn compatible.
In older versions of Rust, dyn compatibility was called "object safety".