From 187f489f907957d8070823da81af11c8dc3f3d9f Mon Sep 17 00:00:00 2001 From: Wojciech Rozowski Date: Thu, 4 Sep 2025 16:44:53 +0100 Subject: [PATCH] Minor changes --- LeroyCompilerVerificationCourse/Constprop.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/LeroyCompilerVerificationCourse/Constprop.lean b/LeroyCompilerVerificationCourse/Constprop.lean index cdf1218..284802c 100644 --- a/LeroyCompilerVerificationCourse/Constprop.lean +++ b/LeroyCompilerVerificationCourse/Constprop.lean @@ -53,7 +53,7 @@ instance [BEq α] [BEq β] [Hashable α] : BEq (Std.HashMap α β) where `mk_MINUS a1 a2` produces an expression equivalent to `MINUS a1 a2` using similar tricks. Note that "expression minus constant" is always normalized into "expression plus opposite constant", - simplifying the case analyses. *) + simplifying the case analyses. -/ @[grind] def mk_MINUS (a1 a2 : aexp) : aexp := match a1, a2 with