From 3e95b30486c146dd9776f9d002c2fbe1f69fb33f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 22 Jan 2026 17:40:10 +0100 Subject: [PATCH] fix: Don't include syntax information in elaboration of math elements This avoids spurious infoview display of the internal elaborated constant type. This bug is only observable after applying the fix in #700 ; will wait for #700 and #699 to merge this so we can properly provide a test. Co-authored-by: David Thrane Christiansen --- src/verso/Verso/Doc/Elab.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/verso/Verso/Doc/Elab.lean b/src/verso/Verso/Doc/Elab.lean index 0313aa2e..a4281c99 100644 --- a/src/verso/Verso/Doc/Elab.lean +++ b/src/verso/Verso/Doc/Elab.lean @@ -194,13 +194,13 @@ public meta def _root_.Lean.Doc.Syntax.code.expand : InlineExpander @[inline_expander Lean.Doc.Syntax.inline_math] public meta def _root_.Lean.Doc.Syntax.inline_math.expand : InlineExpander | `(inline| \math code( $s )) => - ``(Inline.math MathMode.inline $s) + ``(Inline.math MathMode.inline $(quote s.getString)) | _ => throwUnsupportedSyntax @[inline_expander Lean.Doc.Syntax.display_math] public meta def _root_.Lean.Doc.Syntax.display_math.expand : InlineExpander | `(inline| \displaymath code( $s )) => - ``(Inline.math MathMode.display $s) + ``(Inline.math MathMode.display $(quote s.getString)) | _ => throwUnsupportedSyntax