Struct CoqModule 

pub struct CoqModule {
    pub name: String,
    pub requires: Vec<String>,
    pub opens: Vec<String>,
    pub declarations: Vec<CoqDecl>,
}

A complete Coq source file (.v).

Fields

name: String

Top-level module name (used as a comment / Module block if needed)

requires: Vec<String>

Require Import directives emitted before declarations

opens: Vec<String>

Open Scope directives emitted after requires

declarations: Vec<CoqDecl>

Top-level declarations

Implementations

impl CoqModule

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

Construct an empty module.

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

Add a Require Import directive.

pub fn open_scope(&mut self, scope: impl Into<String>)

Add an Open Scope directive.

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

Add a declaration.

pub fn emit(&self) -> String

Emit the full Coq source as a String.

Trait Implementations

impl Clone for CoqModule

fn clone(&self) -> CoqModule

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for CoqModule

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

Formats the value using the given formatter.