Trait Language

pub trait Language:
    'static
    + Copy
    + Ord
    + Hash
    + Debug
    + Default {
    type Kind: Copy + CoreTerm<Self>;
    type Parameter: HasKind<Self> + CoreTerm<Self> + UpcastFrom<CoreVariable<Self>> + UpcastFrom<CoreUniversalVar<Self>> + UpcastFrom<CoreExistentialVar<Self>> + UpcastFrom<CoreBoundVar<Self>>;

    const NAME: &'static str;
    const BINDING_OPEN: char;
    const BINDING_CLOSE: char;
}

The definition of a “language”

Required Associated Constants

const NAME: &'static str

Name of the language, e.g., "Rust"

const BINDING_OPEN: char

The character (typically <) used to open binders.

const BINDING_CLOSE: char

The character (typically >) used to open binders.

Required Associated Types

type Kind: Copy + CoreTerm<Self>

An enum defining the kinds of generic parameters (e.g., for Rust, types, lifetimes, and constants).

type Parameter: HasKind<Self> + CoreTerm<Self> + UpcastFrom<CoreVariable<Self>> + UpcastFrom<CoreUniversalVar<Self>> + UpcastFrom<CoreExistentialVar<Self>> + UpcastFrom<CoreBoundVar<Self>>

An enum defining the value of a generic parameter (e.g., a type, a lifetime, etc)

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors