Struct IdrisProofScript 

pub struct IdrisProofScript {
    pub theorem_name: String,
    pub goal_type: IdrisType,
    pub tactics: Vec<IdrisTactic>,
}

A complete Idris 2 proof in elaborator-reflection style.

Fields

theorem_name: String

The theorem name being proved.

goal_type: IdrisType

The type being proved.

tactics: Vec<IdrisTactic>

Sequence of tactics.

Implementations

impl IdrisProofScript

pub fn new(theorem_name: impl Into<String>, goal_type: IdrisType) -> Self

Create a new proof script.

pub fn push(&mut self, tactic: IdrisTactic)

Append a tactic.

pub fn emit(&self) -> String

Emit the proof as an Idris 2 function definition using proof-by-reflection.

Trait Implementations

impl Clone for IdrisProofScript

fn clone(&self) -> IdrisProofScript

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for IdrisProofScript

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

Formats the value using the given formatter.