Struct ExtractedProgram 

pub struct ExtractedProgram {
    pub source_theorem: String,
    pub program_text: String,
    pub is_complete: bool,
}

An ML-like program extracted from a constructive proof.

Fields

source_theorem: String

The source proposition / theorem.

program_text: String

The program text (pseudo-ML).

is_complete: bool

Whether the extraction is complete.

Implementations

impl ExtractedProgram

pub fn new(theorem: impl Into<String>, program_text: impl Into<String>) -> Self

Create a new extracted program.

Trait Implementations

impl Clone for ExtractedProgram

fn clone(&self) -> ExtractedProgram

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ExtractedProgram

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

Formats the value using the given formatter.