Struct MonotoneFunctionalInterpretation 

pub struct MonotoneFunctionalInterpretation {
    pub formula: String,
    pub majorant: String,
    pub is_bounded: bool,
}

Encodes Kohlenbach’s monotone functional interpretation.

Fields

formula: String

The formula being interpreted.

majorant: String

The majorizing functional (as a description string).

is_bounded: bool

Whether this is a bounded (monotone) interpretation.

Implementations

impl MonotoneFunctionalInterpretation

pub fn new(formula: impl Into<String>, majorant: impl Into<String>) -> Self

Create a new monotone functional interpretation.

pub fn check_bound(&self) -> bool

Check whether the interpretation preserves the monotone bound.

Trait Implementations

impl Clone for MonotoneFunctionalInterpretation

fn clone(&self) -> MonotoneFunctionalInterpretation

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for MonotoneFunctionalInterpretation

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

Formats the value using the given formatter.