We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent c04225e commit 6d65c6eCopy full SHA for 6d65c6e
ProofWidgets/Demos/Graph/MVarGraph.lean
@@ -62,7 +62,7 @@ def mkLabel (e : MVarId)
62
(fill := "var(--vscode-editor-background)") :
63
MetaM (Nat × Nat × Html) := do
64
let fmt := s!"?{← e.getName}"
65
- let fmtTp ← withOptions (·.setNat `pp.deepTerms.threshold 2)
+ let fmtTp ← withOptions (·.set `pp.deepTerms.threshold (2 : Nat))
66
(toString <$> ppExpr (← e.getType'))
67
let len := fmt.length + fmtTp.length + 3
68
let w := min (15 + len * 6) 100
lean-toolchain
@@ -1 +1 @@
1
-leanprover/lean4:v4.27.0
+leanprover/lean4:v4.28.0-rc1
0 commit comments