Enum agda_mode::resp::GoalInfo

pub enum GoalInfo {
    HelperFunction {
        signature: String,
    },
    NormalForm {
        compute_mode: ComputeMode,
        expr: String,
    },
    GoalType(GoalType),
    CurrentGoal {
        rewrite: Rewrite,
        the_type: String,
    },
    InferredType {
        expr: String,
    },
}

Information about one goal.

Variants

HelperFunction

Fields of HelperFunction

signature: String

NormalForm

Fields of NormalForm

compute_mode: ComputeModeexpr: String

GoalType(GoalType)

CurrentGoal

Fields of CurrentGoal

rewrite: Rewritethe_type: String

InferredType

Fields of InferredType

expr: String

Trait Implementations

impl Clone for GoalInfo

pub fn clone(&self) -> GoalInfo

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for GoalInfo

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for GoalInfo

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 GoalInfo

impl PartialEq<GoalInfo> for GoalInfo

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

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

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

This method tests for !=.

impl StructuralEq for GoalInfo

impl StructuralPartialEq for GoalInfo