From 9a970611ca2b2a601378a641e31ae8ead195193b Mon Sep 17 00:00:00 2001 From: Phil de Joux Date: Wed, 21 Feb 2024 17:31:02 -0500 Subject: [PATCH] doc: correct typo "can calls" (#3446) Fixes a minor typo. --- doc/monads/except.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/monads/except.lean b/doc/monads/except.lean index 75da8cf24c..0b91ef477f 100644 --- a/doc/monads/except.lean +++ b/doc/monads/except.lean @@ -33,7 +33,7 @@ convert the pure non-monadic value `x / y` into the required `Except` object. S Now this return typing would get tedious if you had to include it everywhere that you call this function, however, Lean type inference can clean this up. For example, you can define a test -function can calls the `divide` function and you don't need to say anything here about the fact that +function that calls the `divide` function and you don't need to say anything here about the fact that it might throw an error, because that is inferred: -/ def test := divide 5 0