Struct LeanTheorem 

pub struct LeanTheorem {
    pub obligation_name: String,
    pub theorem_name: String,
    pub property: String,
    pub origin_summary: String,
    pub declaration_start_line: usize,
    pub declaration_end_line: usize,
}

Structured Lean theorem metadata derived from an obligation.

Fields

obligation_name: String

theorem_name: String

property: String

origin_summary: String

declaration_start_line: usize

declaration_end_line: usize

Implementations

impl LeanTheorem

pub fn witness_ref(&self, module_name: &str) -> String

pub fn contains_line(&self, line: usize) -> bool

pub fn with_line_span(self, start_line: usize, end_line: usize) -> LeanTheorem

Trait Implementations

impl Clone for LeanTheorem

fn clone(&self) -> LeanTheorem

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LeanTheorem

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

Formats the value using the given formatter.

impl Eq for LeanTheorem

impl From<&Obligation> for LeanTheorem

fn from(obligation: &Obligation) -> LeanTheorem

Converts to this type from the input type.

impl PartialEq for LeanTheorem

fn eq(&self, other: &LeanTheorem) -> 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 StructuralPartialEq for LeanTheorem