Enum Decl 

pub enum Decl {
    Axiom {
        name: String,
        univ_params: Vec<String>,
        ty: Located<SurfaceExpr>,
        attrs: Vec<AttributeKind>,
    },
    Definition {
        name: String,
        univ_params: Vec<String>,
        ty: Option<Located<SurfaceExpr>>,
        val: Located<SurfaceExpr>,
        where_clauses: Vec<WhereClause>,
        attrs: Vec<AttributeKind>,
    },
    Theorem {
        name: String,
        univ_params: Vec<String>,
        ty: Located<SurfaceExpr>,
        proof: Located<SurfaceExpr>,
        where_clauses: Vec<WhereClause>,
        attrs: Vec<AttributeKind>,
    },
    Inductive {
        name: String,
        univ_params: Vec<String>,
        params: Vec<Binder>,
        indices: Vec<Binder>,
        ty: Located<SurfaceExpr>,
        ctors: Vec<Constructor>,
    },
    Import {
        path: Vec<String>,
    },
    Namespace {
        name: String,
        decls: Vec<Located<Decl>>,
    },
    Structure {
        name: String,
        univ_params: Vec<String>,
        extends: Vec<String>,
        fields: Vec<FieldDecl>,
    },
    ClassDecl {
        name: String,
        univ_params: Vec<String>,
        extends: Vec<String>,
        fields: Vec<FieldDecl>,
    },
    InstanceDecl {
        name: Option<String>,
        class_name: String,
        ty: Located<SurfaceExpr>,
        defs: Vec<(String, Located<SurfaceExpr>)>,
    },
    SectionDecl {
        name: String,
        decls: Vec<Located<Decl>>,
    },
    Variable {
        binders: Vec<Binder>,
    },
    Open {
        path: Vec<String>,
        names: Vec<String>,
    },
    Attribute {
        attrs: Vec<String>,
        decl: Box<Located<Decl>>,
    },
    HashCmd {
        cmd: String,
        arg: Located<SurfaceExpr>,
    },
    Mutual {
        decls: Vec<Located<Decl>>,
    },
    Derive {
        instances: Vec<String>,
        type_name: String,
    },
    NotationDecl {
        kind: AstNotationKind,
        prec: Option<u32>,
        name: String,
        notation: String,
    },
    Universe {
        names: Vec<String>,
    },
}

Top-level declaration.

Variants

Axiom

Axiom declaration

Fields

name: String

Name

univ_params: Vec<String>

Universe parameters

ty: Located<SurfaceExpr>

Type

attrs: Vec<AttributeKind>

Attributes

Definition

Definition

Fields

name: String

Name

univ_params: Vec<String>

Universe parameters

ty: Option<Located<SurfaceExpr>>

Type (optional, can be inferred)

val: Located<SurfaceExpr>

Value

where_clauses: Vec<WhereClause>

Where clauses (local definitions)

attrs: Vec<AttributeKind>

Attributes

Theorem

Theorem

Fields

name: String

Name

univ_params: Vec<String>

Universe parameters

ty: Located<SurfaceExpr>

Type (statement)

proof: Located<SurfaceExpr>

Proof

where_clauses: Vec<WhereClause>

Where clauses (local definitions)

attrs: Vec<AttributeKind>

Attributes

Inductive

Inductive type

Fields

name: String

Name

univ_params: Vec<String>

Universe parameters

params: Vec<Binder>

Parameters (non-varying)

indices: Vec<Binder>

Indices (varying)

ty: Located<SurfaceExpr>

Type

ctors: Vec<Constructor>

Constructors

Import

Import declaration

Fields

path: Vec<String>

Module path

Namespace

Namespace declaration

Fields

name: String

Namespace name

decls: Vec<Located<Decl>>

Declarations inside

Structure

Structure declaration

Fields

name: String

Structure name

univ_params: Vec<String>

Universe parameters

extends: Vec<String>

Parent structures (extends)

fields: Vec<FieldDecl>

Fields

ClassDecl

Class declaration

Fields

name: String

Class name

univ_params: Vec<String>

Universe parameters

extends: Vec<String>

Parent classes (extends)

fields: Vec<FieldDecl>

Fields/methods

InstanceDecl

Instance declaration

Fields

name: Option<String>

Optional instance name

class_name: String

Class being instantiated

ty: Located<SurfaceExpr>

The instance type

defs: Vec<(String, Located<SurfaceExpr>)>

Method definitions

SectionDecl

Section declaration

Fields

name: String

Section name

decls: Vec<Located<Decl>>

Declarations inside

Variable

Variable declaration

Fields

binders: Vec<Binder>

Binders

Open

Open declaration

Fields

path: Vec<String>

Module path

names: Vec<String>

Specific names to open (empty = open all)

Attribute

Attribute declaration

Fields

attrs: Vec<String>

Attribute names

decl: Box<Located<Decl>>

Inner declaration

HashCmd

Hash command (#check, #eval, #print)

Fields

cmd: String

Command name (e.g. “check”, “eval”, “print”)

arg: Located<SurfaceExpr>

Argument expression

Mutual

Mutual recursive definitions

Fields

decls: Vec<Located<Decl>>

The mutually recursive declarations

Derive

Derive declaration: deriving instance1, instance2 for TypeName

Fields

instances: Vec<String>

Instance strategies to derive

type_name: String

Type name to derive for

NotationDecl

Notation declaration

Fields

kind: AstNotationKind

Kind of notation

prec: Option<u32>

Precedence (optional)

name: String

Name or symbol

notation: String

Notation body

Universe

Universe declaration: universe u v w

Fields

names: Vec<String>

Universe variable names

Implementations

impl Decl

pub fn name(&self) -> Option<&str>

Get the name of this declaration, if it has one.

pub fn typed_attrs(&self) -> &[AttributeKind]

Get the attributes if this declaration has typed attributes.

pub fn is_mutual(&self) -> bool

Check if this declaration is a mutual block.

Trait Implementations

impl Clone for Decl

fn clone(&self) -> Decl

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Decl

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

Formats the value using the given formatter.

impl PartialEq for Decl

fn eq(&self, other: &Decl) -> 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 Decl