pith. machine review for the scientific record. sign in
structure definition def or abbrev

ProofState

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  38structure ProofState where
  39  /-- Verified propositions (the past). -/
  40  verified : Set Prop
  41  /-- Current proposition being verified (the present). -/
  42  current : Prop
  43  /-- Unverified candidates (the future). -/
  44  unverified : Set Prop
  45  /-- Current is not in past. -/
  46  current_not_in_past : current ∉ verified
  47  /-- Current is not in future (it's the present). -/
  48  current_not_in_future : current ∉ unverified
  49  /-- Future candidates are not yet verified. -/
  50  future_not_verified : ∀ p ∈ unverified, p ∉ verified
  51
  52/-- The recognition step: verify current, move to next. -/

used by (9)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (9)

Lean names referenced from this declaration's body.