Enum Cmd 

pub enum Cmd {
    Load {
        path: String,
        flags: Vec<String>,
    },
    Compile {
        backend: String,
        path: String,
        flags: Vec<String>,
    },
    Constraints,
    Metas,
    ShowModuleContentsToplevel {
        rewrite: Rewrite,
        search: String,
    },
    SearchAboutToplevel {
        rewrite: Rewrite,
        search: String,
    },
    SolveAll(Rewrite),
    SolveOne(InputWithRewrite),
    AutoOne(GoalInput),
    AutoAll,
    InferToplevel {
        rewrite: Rewrite,
        code: String,
    },
    ComputeToplevel {
        compute_mode: ComputeMode,
        code: String,
    },
    LoadHighlightingInfo {
        path: String,
    },
    TokenHighlighting {
        path: String,
        remove: Remove,
    },
    Highlight(GoalInput),
    ShowImplicitArgs(bool),
    ToggleImplicitArgs,
    Give {
        force: UseForce,
        input: GoalInput,
    },
    Refine(GoalInput),
    Intro {
        dunno: bool,
        input: GoalInput,
    },
    RefineOrIntro {
        dunno: bool,
        input: GoalInput,
    },
    Context(InputWithRewrite),
    HelperFunction(InputWithRewrite),
    Infer(InputWithRewrite),
    GoalType(InputWithRewrite),
    ElaborateGive(InputWithRewrite),
    GoalTypeContext(InputWithRewrite),
    GoalTypeContextInfer(InputWithRewrite),
    GoalTypeContextCheck(InputWithRewrite),
    ShowModuleContents(InputWithRewrite),
    MakeCase(GoalInput),
    Compute {
        compute_mode: ComputeMode,
        input: GoalInput,
    },
    WhyInScope(GoalInput),
    WhyInScopeToplevel(String),
    ShowVersion,
    Abort,
}

Variants

Load

Loads the module in file path, using flags as the command-line options.

Fields

path: String

flags: Vec<String>

Compile

Compiles the module in file path using the backend backend, using flags as the command-line options.

Fields

backend: String

path: String

flags: Vec<String>

Constraints

Metas

Show unsolved metas. If there are no unsolved metas but unsolved constraints, show those instead.

ShowModuleContentsToplevel

Shows all the top-level names in the given module, along with their types. Uses the top-level scope.

Fields

rewrite: Rewrite

search: String

SearchAboutToplevel

Shows all the top-level names in scope which mention all the given identifiers in their type.

Fields

rewrite: Rewrite

search: String

SolveAll(Rewrite)

Solve all goals whose values are determined by the constraints.

SolveOne(InputWithRewrite)

Solve the goal at point whose value is determined by the constraints.

AutoOne(GoalInput)

Solve the goal at point by using Auto.

AutoAll

Solve all goals by using Auto.

InferToplevel

Parse the given expression (as if it were defined at the

Fields

rewrite: Rewrite

Normalise the type?

code: String

ComputeToplevel

Parse and type check the given expression (as if it were defined at the top-level of the current module) and normalise it.

Fields

compute_mode: ComputeMode

code: String

LoadHighlightingInfo

loads syntax highlighting information for the module in path, and asks Emacs to apply highlighting info from this file.

If the module does not exist, or its module name is malformed or cannot be determined, or the module has not already been visited, or the cached info is out of date, then no highlighting information is printed.

This command is used to load syntax highlighting information when a new file is opened, and it would probably be annoying if jumping to the definition of an identifier reset the proof state, so this command tries not to do that. One result of this is that the command uses the current include directories, whatever they happen to be.

Fields

path: String

TokenHighlighting

Tells Agda to compute token-based highlighting information for the file.

This command works even if the file’s module name does not match its location in the file system, or if the file is not scope-correct. Furthermore no file names are put in the generated output. Thus it is fine to put source code into a temporary file before calling this command. However, the file extension should be correct.

If the second argument is ‘Remove’, then the (presumably temporary) file is removed after it has been read.

Fields

path: String

remove: Remove

Highlight(GoalInput)

Tells Agda to compute highlighting information for the expression just spliced into an interaction point.

ShowImplicitArgs(bool)

Tells Agda whether or not to show implicit arguments.

ToggleImplicitArgs

Toggle display of implicit arguments.

Give

If the range is ‘noRange’, then the string comes from the minibuffer rather than the goal.

Fields

force: UseForce

input: GoalInput

Refine(GoalInput)

Intro

Fields

dunno: bool

input: GoalInput

RefineOrIntro

Fields

dunno: bool

input: GoalInput

Context(InputWithRewrite)

HelperFunction(InputWithRewrite)

Infer(InputWithRewrite)

GoalType(InputWithRewrite)

ElaborateGive(InputWithRewrite)

Grabs the current goal’s type and checks the expression in the hole against it. Returns the elaborated term.

GoalTypeContext(InputWithRewrite)

Displays the current goal and context.

GoalTypeContextInfer(InputWithRewrite)

Displays the current goal and context and infers the type of an expression.

GoalTypeContextCheck(InputWithRewrite)

Grabs the current goal’s type and checks the expression in the hole against it

ShowModuleContents(InputWithRewrite)

Shows all the top-level names in the given module, along with their types. Uses the scope of the given goal.

MakeCase(GoalInput)

Compute

Fields

compute_mode: ComputeMode

input: GoalInput

WhyInScope(GoalInput)

WhyInScopeToplevel(String)

ShowVersion

Displays version of the running Agda

Abort

Abort the current computation. Does nothing if no computation is in progress.

Implementations

impl Cmd

pub fn load_simple(path: String) -> Self

pub fn goal_type(input: GoalInput) -> Self

Produces CurrentGoal.

pub fn context(input: GoalInput) -> Self

pub fn split(input: GoalInput) -> Self

pub fn search_module(search: String) -> Self

pub fn infer(input: GoalInput) -> Self

Produces InferredType.

pub fn give(input: GoalInput) -> Self

Trait Implementations

impl Clone for Cmd

fn clone(&self) -> Cmd

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Cmd

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

Formats the value using the given formatter.

impl Display for Cmd

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

Formats the value using the given formatter.