Trait formality_core::language::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 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)

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.

Object Safety

This trait is not object safe.

Implementors