From 8f60f1fc3b51cd7af88b01fd047305677733ce87 Mon Sep 17 00:00:00 2001 From: Ramana Kumar Date: Sat, 2 Dec 2023 16:57:45 +0000 Subject: [PATCH] Fix Unicode violation --- src/list/src/rich_listScript.sml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/list/src/rich_listScript.sml b/src/list/src/rich_listScript.sml index ef150aee0a..5f7918a910 100644 --- a/src/list/src/rich_listScript.sml +++ b/src/list/src/rich_listScript.sml @@ -348,7 +348,7 @@ val MAP_FOLDL = Q.store_thm ("MAP_FOLDL", Theorem FOLDL_CONG_invariant: !P f1 f2 l e. P e /\ - (!x a. MEM x l ∧ P a ==> f1 a x = f2 a x /\ P (f2 a x)) + (!x a. MEM x l /\ P a ==> f1 a x = f2 a x /\ P (f2 a x)) ==> FOLDL f1 e l = FOLDL f2 e l /\ P (FOLDL f2 e l) Proof