Function varisat::proof::add_step

pub fn add_step<'a, 's>(
    ctx: Const<VariablesP, Mut<SolverStateP, Mut<ProofP<'a>, Ref<Context<'a>>>>>, 
    solver_vars: bool, 
    step: &'s ProofStep<'s>
)

Add a step to the proof.

Ignored when proof generation is disabled.

When solver_vars is true, all variables and literals will be converted from solver to global vars. Otherwise the proof step needs to use global vars.