Enum ProofPositionSelector 

pub enum ProofPositionSelector {
    Default,
    Index {
        index: u32,
    },
    AfterText {
        text: String,
        occurrence: Option<u32>,
    },
}

Intent selector for one proof position inside a declaration.

Variants

Default

Index

Fields

index: u32

AfterText

Fields

text: String

occurrence: Option<u32>

Trait Implementations

impl Clone for ProofPositionSelector

fn clone(&self) -> ProofPositionSelector

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ProofPositionSelector

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

Formats the value using the given formatter.

impl Default for ProofPositionSelector

fn default() -> ProofPositionSelector

Returns the “default value” for a type.

impl<'lean> IntoLean<'lean> for ProofPositionSelector

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

Allocate (or scalar-box) a Lean representation of self and return the owned handle.

impl PartialEq for ProofPositionSelector

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

Tests for self and other values to be equal, and is used by ==.

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

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for ProofPositionSelector

impl StructuralPartialEq for ProofPositionSelector