public class MinDerivationStep extends MinProofStepStmt
MinProofWorksheet
.
Note: at this time GMFF does not need to know whether a proof step is an
hypothesis or a derivation step, but MinHypothesisStep
and
MinDerivationStep
are provided for completeness and future
possibilities :-)
Constructor and Description |
---|
MinDerivationStep(MinProofWorksheet w,
java.lang.String[][] slc)
Standard MinDerivationStep constructor.
|
buildModelAExport
constructStmt, getCleanedLineString, getCleanedLineString, isChunkWhitespace, typesetFormulaSymbols
public MinDerivationStep(MinProofWorksheet w, java.lang.String[][] slc)
w
- the MinProofworksheet
object which contains the proof
step.slc
- Array of proof step lines each comprised of an Array of
String
s called "chunks", which may be either Metamath
whitespace or Metamath tokens. Hence the acronym "slc" refers
to Statement Line Chunks.