From 7a3ee51d05b9ebbdbcc748a08be14b938df41b3e Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 12 Jun 2022 11:06:50 +0200 Subject: [PATCH] doc: missing word --- doc/notation.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/notation.md b/doc/notation.md index fefb6c24a5..8f6c544db0 100644 --- a/doc/notation.md +++ b/doc/notation.md @@ -20,7 +20,7 @@ this operator should be translated to after the arrow `=>`. The precedence is a natural number describing how "tightly" an operator binds to its arguments, encoding the order of operations. We -can make this more precise by looking at the commands above unfold to: +can make this more precise by looking at what the commands above unfold to: ```lean notation:65 lhs:65 " + " rhs:66 => HAdd.hAdd lhs rhs