Skip to content

Commit 423b317

Browse files
authored
chore: remove dependency of pretty-printing LCNF.LitValue on toExpr (#8408)
1 parent d1ec806 commit 423b317

File tree

1 file changed

+6
-1
lines changed

1 file changed

+6
-1
lines changed

src/Lean/Compiler/LCNF/PrettyPrinter.lean

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -56,10 +56,15 @@ def ppArg (e : Arg) : M Format := do
5656
def ppArgs (args : Array Arg) : M Format := do
5757
prefixJoin " " args ppArg
5858

59+
def ppLitValue (lit : LitValue) : M Format := do
60+
match lit with
61+
| .nat v => return format v
62+
| .str v => return format (repr v)
63+
5964
def ppLetValue (e : LetValue) : M Format := do
6065
match e with
6166
| .erased => return "◾"
62-
| .lit v => ppExpr v.toExpr
67+
| .lit v => ppLitValue v
6368
| .proj _ i fvarId => return f!"{← ppFVar fvarId} # {i}"
6469
| .fvar fvarId args => return f!"{← ppFVar fvarId}{← ppArgs args}"
6570
| .const declName us args => return f!"{← ppExpr (.const declName us)}{← ppArgs args}"

0 commit comments

Comments
 (0)