Struct CtorSpec 

pub struct CtorSpec {
    pub constructor: String,
    pub recursive: Vec<bool>,
}

One constructor of an inductive, as given to ProofState::induction_over: its name and, per positional argument, whether that argument is itself of the inductive type — a recursive position that carries an induction hypothesis. Nil is CtorSpec { constructor: "Nil", recursive: vec![] }; Cons (head then tail) is CtorSpec { constructor: "Cons", recursive: vec![false, true] }.

Fields

constructor: String

The constructor’s name, as registered in the kernel (e.g. "Cons").

recursive: Vec<bool>

One flag per argument, in order: true iff that argument is recursive.

Trait Implementations

impl Clone for CtorSpec

fn clone(&self) -> CtorSpec

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for CtorSpec

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

Formats the value using the given formatter.