Subject: FormalContentKeywords: ::ReferenceEnvironment ::proof ::objectTitle: INF objects--------------------------------------------------An INF object Inf Step Goal Tactic Expression refinementA refinement contains goal, Tactic Expression, Reference Environment, and the refinement result.Refinement result includes subgoals stats xref for tactic expressionAn INF ObjectSee Also: Proofs as Data ⋅--------------------------------------------------Authors: Contributors: RICH:t⋅