Struct LogicalRelation 

pub struct LogicalRelation {
    pub ty: SimpleType,
    /* private fields */
}

A logical relation for a simple type system: maps types to relations between elements of the denotation. Relations are represented as predicate closures.

Fields

ty: SimpleType

Name of the type

Implementations

impl LogicalRelation

pub fn base( name: impl Into<String>, pred: impl Fn(&str, &str) -> bool + 'static, ) -> Self

Build the logical relation for a base type using a supplied predicate.

pub fn arrow(dom: LogicalRelation, cod: LogicalRelation) -> Self

Build the logical relation for A → B from relations for A and B. (f, g) ∈ [A→B] iff ∀ (a,b) ∈ [A], (f a, g b) ∈ [B].

pub fn relates(&self, a: &str, b: &str) -> bool

Test whether a pair of elements are related.

pub fn self_related(&self, term: &str) -> bool

Check the fundamental property: every closed term is related to itself.