From 94c7b021f77c02376ad0219cdef97b1a06bc0d1b Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 15 Jul 2024 12:22:47 -0700 Subject: [PATCH] fix: Signature of ppExpr --- Pantograph/Condensed.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean index f6f4cdb..8b3de4f 100644 --- a/Pantograph/Condensed.lean +++ b/Pantograph/Condensed.lean @@ -20,8 +20,8 @@ def isInaccessible (n: Name) : Bool := n.isInaccessibleUserName @[export pantograph_mk_app_meta_m] def mkAppM (constName : Name) (xs : Array Expr) : MetaM Expr := Meta.mkAppM constName xs -@[export pantograph_pp_expr] -def ppExpr (e: Expr) := Meta.ppExpr e +@[export pantograph_pp_expr_meta_m] +def ppExpr (e: Expr): MetaM String := toString<$> Meta.ppExpr e -- Mirrors Lean's LocalDecl