Struct Instance 

pub struct Instance {
    pub theory: Theory,
    pub stx: FiberTyS,
    pub val: FiberTyV,
    pub codomain: BaseTyV,
}

A toplevel declaration of an instance of a model.

An instance is an object of the fiber over its codomain model X in the comprehension category of D-models: a generator/equation/sub-instance body packaged as the presentation of an X-instance. It is declared with instance NAME : X := [...].

The instance is represented directly as a fiber type — a fiber Record whose fields are its generators (Over), sub-instance imports (nested records), and equations (Id). A sub-instance import we : Edge uses this fiber type directly.

Fields

theory: Theory

The theory that the instance is defined in.

stx: FiberTyS

The syntax of the instance, as a fiber record type.

val: FiberTyV

The value of the instance, as a fiber record type.

codomain: BaseTyV

The codomain model X that this is an instance of.

Implementations

impl Instance

pub const fn new( theory: Theory, stx: FiberTyS, val: FiberTyV, codomain: BaseTyV, ) -> Instance

Trait Implementations

impl Clone for Instance

fn clone(&self) -> Instance

Returns a duplicate of the value.

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

Performs copy-assignment from source.