Enum agda_mode::resp::OutputConstraint

pub enum OutputConstraint<Obj> {
    OfType(OfType<Obj>),
    CmpInType {
        constraint_objs: (Obj, Obj),
        of_type: String,
        comparison: Comparison,
    },
    CmpElim {
        constraint_objs: (Vec<Obj>, Vec<Obj>),
        of_type: String,
        polarities: Vec<Polarity>,
    },
    JustType(JustSomething<Obj>),
    JustSort(JustSomething<Obj>),
    CmpTypes(CmpSomething<Obj>),
    CmpLevels(CmpSomething<Obj>),
    CmpTeles(CmpSomething<Obj>),
    CmpSorts(CmpSomething<Obj>),
    Guard {
        constraint: Box<OutputConstraint<Obj>>,
        problem: ProblemId,
    },
    Assign {
        constraint_obj: Obj,
        value: String,
    },
    TypedAssign(TypedAssign<Obj>),
    PostponedCheckArgs(PostponedCheckArgs<Obj>),
    IsEmptyType {
        the_type: String,
    },
    SizeLtSat {
        the_type: String,
    },
    FindInstanceOF(FindInstanceOF<Obj>),
    PTSInstance {
        constraint_objs: (Obj, Obj),
    },
    PostponedCheckFunDef {
        name: String,
        of_type: String,
    },
}

Variants

OfType(OfType<Obj>)

CmpInType

Fields of CmpInType

constraint_objs: (Obj, Obj)of_type: Stringcomparison: Comparison

CmpElim

Fields of CmpElim

constraint_objs: (Vec<Obj>, Vec<Obj>)of_type: Stringpolarities: Vec<Polarity>

JustType(JustSomething<Obj>)

JustSort(JustSomething<Obj>)

CmpTypes(CmpSomething<Obj>)

CmpLevels(CmpSomething<Obj>)

CmpTeles(CmpSomething<Obj>)

CmpSorts(CmpSomething<Obj>)

Guard

Fields of Guard

constraint: Box<OutputConstraint<Obj>>problem: ProblemId

Assign

Fields of Assign

constraint_obj: Objvalue: String

TypedAssign(TypedAssign<Obj>)

PostponedCheckArgs(PostponedCheckArgs<Obj>)

IsEmptyType

Fields of IsEmptyType

the_type: String

SizeLtSat

Fields of SizeLtSat

the_type: String

FindInstanceOF(FindInstanceOF<Obj>)

PTSInstance

Fields of PTSInstance

constraint_objs: (Obj, Obj)

PostponedCheckFunDef

Fields of PostponedCheckFunDef

name: Stringof_type: String

Methods

impl<Obj> OutputConstraint<Obj>

pub fn try_into_of_type(self) -> Result<OfType<Obj>, Self>

pub fn try_as_of_type(&self) -> Result<&OfType<Obj>, &Self>

Trait Implementations

impl<Obj> CollectObjs<Obj> for OutputConstraint<Obj>

fn collect_objs(&self, collect: impl FnMut(&Obj))

impl<Obj: Clone> Clone for OutputConstraint<Obj>

fn clone(&self) -> OutputConstraint<Obj>

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<Obj: Eq> Eq for OutputConstraint<Obj>

impl<Obj: PartialEq> PartialEq<OutputConstraint<Obj>> for OutputConstraint<Obj>

fn eq(&self, other: &OutputConstraint<Obj>) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &OutputConstraint<Obj>) -> bool

This method tests for !=.

impl<Obj: Display + Debug> Display for OutputConstraint<Obj>

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

Formats the value using the given formatter.

impl<Obj: Debug> Debug for OutputConstraint<Obj>

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

Formats the value using the given formatter.

impl<Obj> StructuralPartialEq for OutputConstraint<Obj>

impl<Obj> StructuralEq for OutputConstraint<Obj>

impl<'de, Obj> Deserialize<'de> for OutputConstraint<Obj> where
    Obj: Deserialize<'de>, 

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error> where
    __D: Deserializer<'de>, 

Deserialize this value from the given Serde deserializer.