Proof Utilities

ProofLine(line::Int, statement::AbstractExpression, argument::A, references::Vector{ProofLine}) where {A}

Represents a single line in a step-by-step proof, made up by a statement, an argument, and a set of references necessary to make the provided argument. A line number is also required to serve as a unique human-readable identifier for each line.

ProofLine(line::Int, statement::AbstractExpression, argument::A="N/A") where {A}

Creates a ProofLine without any references to other lines and without an argument. Implicitly this means in most proofs that this line depends only on the previous one, but can also be taken to mean "is a conclusion of all statements above".

ProofLine(line::Int, statement::AbstractExpression, argument::A, reference::ProofLine{A}) where {A}

Convenience method. Creates a ProofLine with a single provided reference instead of a list of them.