Skip to content

Commit f0b3119

Browse files
kim-emclaude
andauthored
fix: use KVMap.setBool instead of private Options constructor (#351)
The Lean.Options constructor is now private, so we can no longer use `⟨...⟩` notation. Use KVMap.empty with chained .setBool calls instead. Co-authored-by: Claude Opus 4.5 <[email protected]>
1 parent 01e1433 commit f0b3119

File tree

1 file changed

+6
-6
lines changed

1 file changed

+6
-6
lines changed

DocGen4/Load.lean

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -28,12 +28,12 @@ def load (task : Process.AnalyzeTask) : IO (Process.AnalyzerResult × Hierarchy)
2828
let config := {
2929
-- TODO: parameterize maxHeartbeats
3030
maxHeartbeats := 100000000,
31-
options := ⟨[
32-
(`pp.tagAppFns, true),
33-
(`pp.funBinderTypes, true),
34-
(`debug.skipKernelTC, true),
35-
(`Elab.async, false)
36-
]⟩,
31+
options :=
32+
Options.empty
33+
|>.setBool `pp.tagAppFns true
34+
|>.setBool `pp.funBinderTypes true
35+
|>.setBool `debug.skipKernelTC true
36+
|>.setBool `Elab.async false,
3737
-- TODO: Figure out whether this could cause some bugs
3838
fileName := default,
3939
fileMap := default,

0 commit comments

Comments
 (0)