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

doc: fix docstring typos (#2605)

Browse source 
* lake: fix a typo in `get_config?` syntax doc
* fix a typo in `withImporting` doc
This commit is contained in:
Denis Gorbachev 2023-09-30 18:51:35 +07:00 • committed by GitHub
parent 06e057758e
commit e6292bc0b8
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/ImportingFlag.lean
View file

@ -42,7 +42,7 @@ the `initialize` command to update global references.
IMPORTANT: There is no semaphore controlling the access to these global references.
We assume these global references are updated by a single execution thread.
This is true in the Lean frontend where we process the `import` commands at the beginning
of the execution only. Users must make sure that `importModules` is used, there is only
of the execution only. Users must make sure that when `importModules` is used, there is only
one execution thread accessing the global references.
-/
def withImporting (x : IO α) : IO α :=

2
src/lake/Lake/DSL/Config.lean
View file

@ -40,7 +40,7 @@ def elabDirConst : TermElab := fun stx expectedType? => do
/--
A macro that expands to the specified configuration option (or `none`,
if not the option has not been set) during the Lakefile's elaboration.
if the option has not been set) during the Lakefile's elaboration.
Configuration arguments are set either via the Lake CLI (by the `-K` option)
or via the `with` clause in a `require` statement.