lib/monads/trace: add comment for prefix_closed

Signed-off-by: Corey Lewis <[email protected]>
seL4 · Mar 26, 2024 · 8777671 · 8777671
1 parent 040fd7d
commit 8777671
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/lib/Monads/trace/Trace_Prefix_Closed.thy b/lib/Monads/trace/Trace_Prefix_Closed.thy
@@ -14,6 +14,9 @@ begin
 
 subsection "Prefix Closed"
 
+text \<open>
+  A monad is @{text prefix_closed} if for all traces that it returns, it also returns all incomplete traces
+  leading up to it.\<close>
 definition prefix_closed :: "('s, 'a) tmonad \<Rightarrow> bool" where
   "prefix_closed f = (\<forall>s. \<forall>x xs. (x # xs) \<in> fst ` f s \<longrightarrow> (xs, Incomplete) \<in> f s)"