Struct CoqContext 

pub struct CoqContext {
    pub vars: Vec<CoqSectionVar>,
    pub hyps: Vec<CoqHypothesis>,
}

Coq context (list of section vars + hypotheses)

Fields

vars: Vec<CoqSectionVar>

hyps: Vec<CoqHypothesis>

Implementations

impl CoqContext

pub fn new() -> Self

pub fn add_var(&mut self, v: CoqSectionVar)

pub fn add_hyp(&mut self, h: CoqHypothesis)

pub fn emit(&self) -> String

Trait Implementations

impl Debug for CoqContext

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

Formats the value using the given formatter.

impl Default for CoqContext

fn default() -> CoqContext

Returns the “default value” for a type.