Enum AgdaDecl 

pub enum AgdaDecl {
    FuncType {
        name: String,
        ty: AgdaExpr,
    },
    FuncDef {
        name: String,
        clauses: Vec<AgdaClause>,
    },
    DataDecl(AgdaData),
    RecordDecl(AgdaRecord),
    ModuleDecl {
        name: String,
        params: Vec<(String, AgdaExpr)>,
        body: Vec<AgdaDecl>,
    },
    Import(String),
    Open(String),
    Variable(Vec<(String, AgdaExpr)>),
    Postulate(Vec<(String, AgdaExpr)>),
    Pragma(String),
    Comment(String),
    Raw(String),
}

Top-level Agda 2 declaration.

Variants

FuncType

Type signature: f : T

Fields

name: String

ty: AgdaExpr

FuncDef

Function definition: one or more clauses

Fields

name: String

clauses: Vec<AgdaClause>

DataDecl(AgdaData)

Data declaration

RecordDecl(AgdaRecord)

Record declaration

ModuleDecl

Module declaration: module M where ...

Fields

name: String

params: Vec<(String, AgdaExpr)>

body: Vec<AgdaDecl>

Import(String)

import Data.Nat

Open(String)

open Data.Nat (or open Data.Nat using (...))

Variable(Vec<(String, AgdaExpr)>)

variable {A B : Set}

Postulate(Vec<(String, AgdaExpr)>)

postulate name : T

Pragma(String)

{-# BUILTIN ... #-} pragma

Comment(String)

Plain comment: -- text

Raw(String)

Raw verbatim Agda text (fallback)

Implementations

impl AgdaDecl

pub fn emit(&self, indent: usize) -> String

Emit as an Agda source string at the given indentation level.

Trait Implementations

impl Clone for AgdaDecl

fn clone(&self) -> AgdaDecl

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for AgdaDecl

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

Formats the value using the given formatter.

impl PartialEq for AgdaDecl

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

Tests for self and other values to be equal, and is used by ==.

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

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for AgdaDecl