Struct DeclarationSearchRequest

Source

pub struct DeclarationSearchRequest {
    pub name_fragment: Option<String>,
    pub name_match: DeclarationNameMatch,
    pub kind: Option<String>,
    pub required_constants: Vec<String>,
    pub conclusion_head: Option<String>,
    pub scope_biases: Vec<DeclarationSearchBias>,
    pub limit: usize,
    pub filter: LeanDeclarationFilter,
    pub include_source: bool,
}

Fields§

§name_fragment: Option<String>§name_match: DeclarationNameMatch§kind: Option<String>§required_constants: Vec<String>§conclusion_head: Option<String>§scope_biases: Vec<DeclarationSearchBias>§limit: usize§filter: LeanDeclarationFilter§include_source: bool

Struct DeclarationSearchRequest Copy item path

Fields§

Implementations§

impl DeclarationSearchRequest

pub fn new(name_fragment: impl Into<String>) -> Self

Trait Implementations§

impl Clone for DeclarationSearchRequest

fn clone(&self) -> DeclarationSearchRequest

fn clone_from(&mut self, source: &Self)

impl Debug for DeclarationSearchRequest

fn fmt(&self, f: &mut Formatter<'_>) -> Result

impl Eq for DeclarationSearchRequest

impl<'lean> IntoLean<'lean> for DeclarationSearchRequest

fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean>

impl<'lean> LeanAbi<'lean> for DeclarationSearchRequest

type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr

impl<'lean> LeanAbi<'lean> for &DeclarationSearchRequest

type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr

impl PartialEq for DeclarationSearchRequest

fn eq(&self, other: &DeclarationSearchRequest) -> bool

fn ne(&self, other: &Rhs) -> bool

impl SealedAbi for DeclarationSearchRequest

impl SealedAbi for &DeclarationSearchRequest

impl StructuralPartialEq for DeclarationSearchRequest

Auto Trait Implementations§

impl Freeze for DeclarationSearchRequest

impl RefUnwindSafe for DeclarationSearchRequest

impl Send for DeclarationSearchRequest

impl Sync for DeclarationSearchRequest

impl Unpin for DeclarationSearchRequest

impl UnsafeUnpin for DeclarationSearchRequest

impl UnwindSafe for DeclarationSearchRequest

Blanket Implementations§

impl<T> Any for Twhere T: 'static + ?Sized,

fn type_id(&self) -> TypeId

impl<T> Borrow<T> for Twhere T: ?Sized,

fn borrow(&self) -> &T

impl<T> BorrowMut<T> for Twhere T: ?Sized,

fn borrow_mut(&mut self) -> &mut T

impl<T> CloneToUninit for Twhere T: Clone,

unsafe fn clone_to_uninit(&self, dest: *mut u8)

impl<'lean, T> DecodeCallResult<'lean> for Twhere T: LeanAbi<'lean>,

const EXPECTS_IO_RESULT: bool = false

type Output = T

type CRepr = <T as LeanAbi<'lean>>::CRepr

fn export_abi_return() -> LeanExportReturnAbi

fn decode_c( c: <T as LeanAbi<'lean>>::CRepr, runtime: &'lean LeanRuntime, ) -> Result<T, LeanError>

impl<T> From<T> for T

fn from(t: T) -> T

impl<T> Instrument for T

fn instrument(self, span: Span) -> Instrumented<Self>

fn in_current_span(self) -> Instrumented<Self>

impl<T, U> Into<U> for Twhere U: From<T>,

fn into(self) -> U

impl<T> Same for T

type Output = T

impl<T> ToOwned for Twhere T: Clone,

type Owned = T

fn to_owned(&self) -> T

fn clone_into(&self, target: &mut T)

impl<T, U> TryFrom<U> for Twhere U: Into<T>,

type Error = Infallible

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

impl<T, U> TryInto<U> for Twhere U: TryFrom<T>,

type Error = <U as TryFrom<T>>::Error

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

impl<T> WithSubscriber for T

fn with_subscriber<S>(self, subscriber: S) -> WithDispatch<Self>where S: Into<Dispatch>,

fn with_current_subscriber(self) -> WithDispatch<Self>

Struct DeclarationSearchRequest

impl<T> Any for T
where T: 'static + ?Sized,

impl<T> Borrow<T> for T
where T: ?Sized,

impl<T> BorrowMut<T> for T
where T: ?Sized,

impl<T> CloneToUninit for T
where T: Clone,

impl<'lean, T> DecodeCallResult<'lean> for T
where T: LeanAbi<'lean>,

impl<T, U> Into<U> for T
where U: From<T>,

impl<T> ToOwned for T
where T: Clone,

impl<T, U> TryFrom<U> for T
where U: Into<T>,

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

fn with_subscriber<S>(self, subscriber: S) -> WithDispatch<Self>
where S: Into<Dispatch>,