From 3614d8e388ceea3065ec7a215a2ea18830bcca63 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 10 Jan 2021 10:51:00 +0100 Subject: [PATCH] doc: typo --- doc/nat.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/nat.md b/doc/nat.md index 5ec51fe243..6b5cbdaf8e 100644 --- a/doc/nat.md +++ b/doc/nat.md @@ -60,7 +60,7 @@ theorem ex ``` The sharp-eyed reader will notice that GMP is part of the Lean kernel trusted code base. We believe this is not a problem because you can use external type checkers to double-check your developments, -and we consider GMP very thrustworthy. +and we consider GMP very trustworthy. Existing external type checkers for Lean 3 (e.g., [Trepplein](https://github.com/gebner/trepplein) and [TC](https://github.com/leanprover/tc)) can be easily adapted to Lean 4. If you are still concerned after checking your development with multiple different external checkers because