Add SOS module for SOS semantics and update ProbabilisticPrograms imports

HEIGE-PCloud · HEIGE-PCloud · commit 9a1392f666d6 · 2026-03-17T22:28:59.000Z
diff --git a/ProgramAnalysis/ProbabilisticPrograms.lean b/ProgramAnalysis/ProbabilisticPrograms.lean
@@ -1,3 +1,4 @@
 module
 
 public import ProgramAnalysis.ProbabilisticPrograms.PWhile
+public import ProgramAnalysis.ProbabilisticPrograms.SOS
diff --git a/ProgramAnalysis/ProbabilisticPrograms/SOS.lean b/ProgramAnalysis/ProbabilisticPrograms/SOS.lean
@@ -0,0 +1,3 @@
+module
+
+/-! # SOS Semantics -/

Original file line number	Diff line number	Diff line change
`@@ -1,3 +1,4 @@`
`1`	`1`	`module`
`2`	`2`
`3`	`3`	`public import ProgramAnalysis.ProbabilisticPrograms.PWhile`
	`4`	`+public import ProgramAnalysis.ProbabilisticPrograms.SOS`