From 877767185ad5ddd640c56950ef092930762ecdd4 Mon Sep 17 00:00:00 2001
From: Corey Lewis <corey.lewis@proofcraft.systems>
Date: Thu, 14 Mar 2024 15:52:48 +1100
Subject: [PATCH] lib/monads/trace: add comment for prefix_closed

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
---
 lib/Monads/trace/Trace_Prefix_Closed.thy | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/lib/Monads/trace/Trace_Prefix_Closed.thy b/lib/Monads/trace/Trace_Prefix_Closed.thy
index 04e0a90f0f..7e7ab925e5 100644
--- 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)"