Enum FnObjHead 

pub enum FnObjHead {
    Identifier(Identifier),
    IdentifierWithMod(IdentifierWithMod),
    Forall(ForallFreeParamObj),
    DefHeader(DefHeaderFreeParamObj),
    Exist(ExistFreeParamObj),
    SetBuilder(SetBuilderFreeParamObj),
    FnSet(FnSetFreeParamObj),
    AnonymousFnLiteral(Box<AnonymousFn>),
    Induc(ByInducFreeParamObj),
    DefAlgo(DefAlgoFreeParamObj),
}

Function-application head: plain identifier pieces or tagged free-parameter binders.

Variants

Identifier(Identifier)

IdentifierWithMod(IdentifierWithMod)

Forall(ForallFreeParamObj)

DefHeader(DefHeaderFreeParamObj)

Exist(ExistFreeParamObj)

SetBuilder(SetBuilderFreeParamObj)

FnSet(FnSetFreeParamObj)

AnonymousFnLiteral(Box<AnonymousFn>)

Anonymous function literal used as applied head, e.g. '(x R) R {x}(a).

Induc(ByInducFreeParamObj)

DefAlgo(DefAlgoFreeParamObj)

Implementations

impl FnObjHead

pub fn from_name_obj(obj: Obj) -> Option<FnObjHead>

If obj is a plain name shape, returns the corresponding function head; otherwise None.

Trait Implementations

impl Clone for FnObjHead

fn clone(&self) -> FnObjHead

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Display for FnObjHead

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

Formats the value using the given formatter.

impl From<ByInducFreeParamObj> for FnObjHead

fn from(p: ByInducFreeParamObj) -> Self

Converts to this type from the input type.

impl From<DefAlgoFreeParamObj> for FnObjHead

fn from(p: DefAlgoFreeParamObj) -> Self

Converts to this type from the input type.

impl From<DefHeaderFreeParamObj> for FnObjHead

fn from(p: DefHeaderFreeParamObj) -> Self

Converts to this type from the input type.

impl From<ExistFreeParamObj> for FnObjHead

fn from(p: ExistFreeParamObj) -> Self

Converts to this type from the input type.

impl From<FnObjHead> for Obj

fn from(h: FnObjHead) -> Self

Converts to this type from the input type.

impl From<FnSetFreeParamObj> for FnObjHead

fn from(p: FnSetFreeParamObj) -> Self

Converts to this type from the input type.

impl From<ForallFreeParamObj> for FnObjHead

fn from(p: ForallFreeParamObj) -> Self

Converts to this type from the input type.

impl From<SetBuilderFreeParamObj> for FnObjHead

fn from(p: SetBuilderFreeParamObj) -> Self

Converts to this type from the input type.