We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 60afb25 commit 4d95055Copy full SHA for 4d95055
1 file changed
DatapathVerification/BitHeap/Chain.lean
@@ -37,7 +37,7 @@ def ChainPreconditions (steps : List Adder) (h : BitHeap) : Prop :=
37
∧ ChainPreconditions rest (applyAdder s h)
38
39
/-- Main correctness theorem for the chain.
40
- Applying the chain preserves the heap's value under all evaluation environments-/
+ Applying the chain preserves the heap's value under all evaluation environments -/
41
theorem applyChain_correct (steps : List Adder) (h : BitHeap)
42
(hwf : ChainPreconditions steps h) :
43
∀ (env : BitEnv), (applyChain steps h).eval env = h.eval env := by
0 commit comments