We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent d560041 commit be024c8Copy full SHA for be024c8
Auto/Tactic.lean
@@ -331,7 +331,6 @@ def addTryThisTacticSeqSuggestion (ref : Syntax) (suggestion : TSyntax ``Lean.Pa
331
if let some range := (origSpan?.getD ref).getRange? then
332
let map ← getFileMap
333
let (indent, column) := Lean.Meta.Tactic.TryThis.getIndentAndColumn map range
334
- dbg_trace s!"indent: {indent}, column: {column}"
335
let text := fmt.pretty (width := Std.Format.defWidth) indent column
336
let suggestion := {
337
-- HACK: The `tacticSeq` syntax category is pretty-printed with each line
0 commit comments