Struct agda_mode::resp::GoalType

pub struct GoalType {
    pub rewrite: Rewrite,
    pub type_aux: GoalTypeAux,
    pub the_type: String,
    pub entries: Vec<ResponseContextEntry>,
    pub boundary: Vec<String>,
    pub output_forms: Vec<String>,
}

Fields

rewrite: Rewrite

type_aux: GoalTypeAux

the_type: String

entries: Vec<ResponseContextEntry>

boundary: Vec<String>

output_forms: Vec<String>

Trait Implementations

impl Clone for GoalType

pub fn clone(&self) -> GoalType

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for GoalType

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for GoalType

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 GoalType

impl PartialEq<GoalType> for GoalType

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

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

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

This method tests for !=.

impl StructuralEq for GoalType

impl StructuralPartialEq for GoalType