Enum CoqDecl 

pub enum CoqDecl {
    Definition {
        name: String,
        params: Vec<(String, CoqTerm)>,
        ty: Option<CoqTerm>,
        body: CoqTerm,
    },
    Theorem {
        name: String,
        params: Vec<(String, CoqTerm)>,
        ty: CoqTerm,
        proof: CoqProof,
    },
    Lemma {
        name: String,
        params: Vec<(String, CoqTerm)>,
        ty: CoqTerm,
        proof: CoqProof,
    },
    Axiom {
        name: String,
        ty: CoqTerm,
    },
    Inductive(CoqInductive),
    Fixpoint(Vec<CoqFixPoint>),
    RecordDecl(CoqRecord),
    ClassDecl(CoqClass),
    Instance(CoqInstance),
    Require(String),
    OpenScope(String),
    Notation(String, CoqTerm),
    Comment(String),
    Raw(String),
}

Top-level Coq declaration.

Variants

Definition

Definition f (params) : T := body.

Fields

name: String

params: Vec<(String, CoqTerm)>

ty: Option<CoqTerm>

body: CoqTerm

Theorem

Theorem name (params) : T. Proof. ... Qed.

Fields

name: String

params: Vec<(String, CoqTerm)>

ty: CoqTerm

proof: CoqProof

Lemma

Lemma name (params) : T. Proof. ... Qed.

Fields

name: String

params: Vec<(String, CoqTerm)>

ty: CoqTerm

proof: CoqProof

Axiom

Axiom name : T.

Fields

name: String

ty: CoqTerm

Inductive(CoqInductive)

Inductive name params : Sort := constructors.

Fixpoint(Vec<CoqFixPoint>)

Fixpoint f params : T := body. (possibly mutual)

RecordDecl(CoqRecord)

Record name params : Sort := { fields }.

ClassDecl(CoqClass)

Class name params := { methods }.

Instance(CoqInstance)

Instance name : class := { methods }.

Require(String)

Require Import module.

OpenScope(String)

Open Scope scope_name.

Notation(String, CoqTerm)

Notation "..." := term.

Comment(String)

A raw comment line

Raw(String)

A raw verbatim declaration (fallback)

Implementations

impl CoqDecl

pub fn emit(&self) -> String

Emit the declaration as a Coq source string.

Trait Implementations

impl Clone for CoqDecl

fn clone(&self) -> CoqDecl

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for CoqDecl

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

Formats the value using the given formatter.

impl PartialEq for CoqDecl

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