We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 9f0f3bc commit 80d4556Copy full SHA for 80d4556
LeroyCompilerVerificationCourse/Constprop.lean
@@ -53,7 +53,7 @@ instance [BEq α] [BEq β] [Hashable α] : BEq (Std.HashMap α β) where
53
`mk_MINUS a1 a2` produces an expression equivalent to `MINUS a1 a2`
54
using similar tricks. Note that "expression minus constant" is
55
always normalized into "expression plus opposite constant",
56
- simplifying the case analyses. *)
+ simplifying the case analyses.
57
-/
58
@[grind] def mk_MINUS (a1 a2 : aexp) : aexp :=
59
match a1, a2 with
0 commit comments