Skip to content

Commit

Permalink
use a better name
Browse files Browse the repository at this point in the history
  • Loading branch information
LeventErkok committed Aug 29, 2024
1 parent d9cacb7 commit 5ab8c4f
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions Documentation/SBV/Examples/KnuckleDragger/Kleene.hs
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,7 @@ x <= y = x + y .== y
--
-- We have:
--
-- >>> example
-- >>> kleeneProofs
-- Axiom: par_assoc Admitted.
-- Axiom: par_comm Admitted.
-- Axiom: par_idem Admitted.
Expand All @@ -85,8 +85,8 @@ x <= y = x + y .== y
-- Lemma: star_star_2_3 Q.E.D.
-- Lemma: star_star_2_1 Q.E.D.
-- Lemma: star_star_2 Q.E.D.
example :: IO ()
example = do
kleeneProofs :: IO ()
kleeneProofs = do

-- Kozen axioms
par_assoc <- axiom "par_assoc" $ \(Forall (x :: SKleene)) (Forall y) (Forall z) -> x + (y + z) .== (x + y) + z
Expand Down

0 comments on commit 5ab8c4f

Please sign in to comment.