max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: typo

Browse source
This commit is contained in:
Sebastian Ullrich 2021-01-10 10:51:00 +01:00
parent 873634be7e
commit 3614d8e388
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
doc/nat.md
View file

@ -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