Struct SemanticTranslation 

pub struct SemanticTranslation {
    pub entry: Option<String>,
    pub observation_procedure: &'static str,
    pub encodings: Vec<Encoding>,
    pub assumptions: Vec<Assumption>,
    pub obligations: Vec<TranslationObligation>,
    pub mappings: Vec<Mapping>,
    pub runtime_dependencies: Vec<String>,
    pub provenance: TranslationProvenance,
}

The record of one semantic translation.

Fields

entry: Option<String>

The target’s entry point, when the source has a main program.

observation_procedure: &'static str

How the target’s observations are made.

encodings: Vec<Encoding>

Representation choices for constructs without a direct target equivalent.

assumptions: Vec<Assumption>

Assumptions, with the program-specific details.

obligations: Vec<TranslationObligation>

Source theorems and assertions and how the target discharges them.

mappings: Vec<Mapping>

Where each source declaration went, with its source span in UTF-16 code units.

runtime_dependencies: Vec<String>

Libraries and host features the emitted program needs.

provenance: TranslationProvenance

Where the translation came from.

Trait Implementations

impl Clone for SemanticTranslation

fn clone(&self) -> SemanticTranslation

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for SemanticTranslation

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

Formats the value using the given formatter.

impl Eq for SemanticTranslation

impl PartialEq for SemanticTranslation

fn eq(&self, other: &SemanticTranslation) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl StructuralPartialEq for SemanticTranslation