Struct AgdaModule 

pub struct AgdaModule {
    pub module_name: String,
    pub params: Vec<(String, AgdaExpr)>,
    pub imports: Vec<String>,
    pub opens: Vec<String>,
    pub declarations: Vec<AgdaDecl>,
}

A complete Agda 2 source file.

Fields

module_name: String

Top-level module name (must match filename without .agda extension)

params: Vec<(String, AgdaExpr)>

Module-level parameters (for parameterised modules)

imports: Vec<String>

import directives

opens: Vec<String>

open directives (after imports)

declarations: Vec<AgdaDecl>

Top-level declarations

Implementations

impl AgdaModule

pub fn new(module_name: impl Into<String>) -> Self

Construct an empty module.

pub fn import(&mut self, module: impl Into<String>)

Add an import.

pub fn open(&mut self, module: impl Into<String>)

Add an open.

pub fn add(&mut self, decl: AgdaDecl)

Add a declaration.

pub fn emit(&self) -> String

Emit the full Agda 2 source as a String.

Trait Implementations

impl Clone for AgdaModule

fn clone(&self) -> AgdaModule

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for AgdaModule

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

Formats the value using the given formatter.