Struct Discouragements

pub struct Discouragements {
    pub modification_discouraged: bool,
    pub usage_discouraged: bool,
}

Discouragement information about a theorem.

Fields

modification_discouraged: bool

Is proof modification discouraged for this theorem?

usage_discouraged: bool

Is new usage discouraged for this theorem?

Implementations

impl Discouragements

pub fn new(buf: &[u8]) -> Self

Parse the text of a statement’s comment to determine whether proof usage or modification is discouraged.

Trait Implementations

impl Clone for Discouragements

fn clone(&self) -> Discouragements

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Discouragements

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

Formats the value using the given formatter.

impl Default for Discouragements

fn default() -> Discouragements

Returns the “default value” for a type.

impl PartialEq for Discouragements

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

impl Eq for Discouragements

impl StructuralPartialEq for Discouragements