fix(doc): remove misplaced capital letter
This commit is contained in:
parent
7202e076dd
commit
dd0a8b7743
1 changed files with 1 additions and 1 deletions
|
@ -371,7 +371,7 @@ examples.
|
||||||
#+END_SRC
|
#+END_SRC
|
||||||
|
|
||||||
In many cases, Lean can automatically infer the type of the variable. Actually,
|
In many cases, Lean can automatically infer the type of the variable. Actually,
|
||||||
In all examples above, the type can be inferred automatically.
|
in all examples above, the type can be inferred automatically.
|
||||||
|
|
||||||
#+BEGIN_SRC lean
|
#+BEGIN_SRC lean
|
||||||
import data.nat
|
import data.nat
|
||||||
|
|
Loading…
Reference in a new issue