Struct UnwindingResult 

pub struct UnwindingResult {
    pub classical_proof: String,
    pub constructive_content: String,
    pub interpreter_used: String,
}

Unwinding theorem: proof mining extracts computational content.

Fields

classical_proof: String

constructive_content: String

interpreter_used: String

Implementations

impl UnwindingResult

pub fn new(classical: &str, constructive: &str, interp: &str) -> Self

pub fn kohlenbach_style(&self) -> String

Trait Implementations

impl Clone for UnwindingResult

fn clone(&self) -> UnwindingResult

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for UnwindingResult

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

Formats the value using the given formatter.