We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 6301b33 commit a1b980fCopy full SHA for a1b980f
src/Lean/Environment.lean
@@ -924,7 +924,7 @@ def setState {σ : Type} (ext : EnvExtension σ) (env : Environment) (s : σ) :
924
925
-- `unsafe` fails to infer `Nonempty` here
926
private unsafe def getStateUnsafe {σ : Type} [Inhabited σ] (ext : EnvExtension σ)
927
- (env : Environment) (asyncMode := ext.asyncMode) : σ :=
+ (env : Environment) (asyncMode : AsyncMode) : σ :=
928
-- safety: `ext`'s constructor is private, so we can assume the entry at `ext.idx` is of type `σ`
929
match asyncMode with
930
| .sync => ext.getStateImpl env.checked.get.extensions
0 commit comments