pub struct Dependence { /* private fields */ }Expand description
Whether a node depends on declarations of a kind, directly or not.
Implementations§
Source§impl Dependence
impl Dependence
Sourcepub fn numbers(program: &Program) -> Self
pub fn numbers(program: &Program) -> Self
Whether a node computes with JavaScript Numbers: it has a Number-typed part, or uses a declaration that does.
Sourcepub fn partial(program: &Program) -> Self
pub fn partial(program: &Program) -> Self
Whether a node calls a recursive function with no decreasing argument: Lean defines those as partial defs, whose equations the kernel cannot unfold.
pub fn prop(&self, prop: &Prop) -> bool
pub fn expr(&self, expr: &Expr) -> bool
Auto Trait Implementations§
impl Freeze for Dependence
impl RefUnwindSafe for Dependence
impl Send for Dependence
impl Sync for Dependence
impl Unpin for Dependence
impl UnsafeUnpin for Dependence
impl UnwindSafe for Dependence
Blanket Implementations§
§impl<T> ArchivePointee for T
impl<T> ArchivePointee for T
§type ArchivedMetadata = ()
type ArchivedMetadata = ()
The archived version of the pointer metadata for this type.
§fn pointer_metadata(
_: &<T as ArchivePointee>::ArchivedMetadata,
) -> <T as Pointee>::Metadata
fn pointer_metadata( _: &<T as ArchivePointee>::ArchivedMetadata, ) -> <T as Pointee>::Metadata
Converts some archived metadata to the pointer metadata for itself.
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more
Source§impl<T> IntoEither for T
impl<T> IntoEither for T
Source§fn into_either(self, into_left: bool) -> Either<Self, Self> ⓘ
fn into_either(self, into_left: bool) -> Either<Self, Self> ⓘ
Converts
self into a Left variant of Either<Self, Self>
if into_left is true.
Converts self into a Right variant of Either<Self, Self>
otherwise. Read moreSource§fn into_either_with<F>(self, into_left: F) -> Either<Self, Self> ⓘ
fn into_either_with<F>(self, into_left: F) -> Either<Self, Self> ⓘ
Converts
self into a Left variant of Either<Self, Self>
if into_left(&self) returns true.
Converts self into a Right variant of Either<Self, Self>
otherwise. Read more§impl<T> LayoutRaw for T
impl<T> LayoutRaw for T
§fn layout_raw(_: <T as Pointee>::Metadata) -> Result<Layout, LayoutError>
fn layout_raw(_: <T as Pointee>::Metadata) -> Result<Layout, LayoutError>
Returns the layout of the type.