Enum agda_mode::resp::GoalTypeAux

pub enum GoalTypeAux {
    GoalOnly,
    GoalAndHave {
        expr: String,
    },
    GoalAndElaboration {
        term: String,
    },
}

Variants

GoalOnly

GoalAndHave

Fields of GoalAndHave

expr: String

GoalAndElaboration

Fields of GoalAndElaboration

term: String

Trait Implementations

impl Clone for GoalTypeAux

pub fn clone(&self) -> GoalTypeAux

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for GoalTypeAux

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for GoalTypeAux

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

Deserialize this value from the given Serde deserializer.

impl Eq for GoalTypeAux

impl PartialEq<GoalTypeAux> for GoalTypeAux

pub fn eq(&self, other: &GoalTypeAux) -> bool

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

pub fn ne(&self, other: &GoalTypeAux) -> bool

This method tests for !=.

impl StructuralEq for GoalTypeAux

impl StructuralPartialEq for GoalTypeAux