From c9ee31bbfdd215e5ceba960218c8344afd46954e Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 2 Aug 2024 22:33:03 -0700 Subject: [PATCH] feat: Export `mkFun` --- Pantograph/Condensed.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean index 9c20f32..8696523 100644 --- a/Pantograph/Condensed.lean +++ b/Pantograph/Condensed.lean @@ -25,6 +25,14 @@ def isInaccessible (n: Name) : Bool := n.isInaccessibleUserName || n.hasMacroSco def mkAppM (constName : Name) (xs : Array Expr) : MetaM Expr := Meta.mkAppM constName xs @[export pantograph_mk_app_expr_m] def mkAppM' (f: Expr) (xs : Array Expr) : MetaM Expr := Meta.mkAppM' f xs +-- Copies same function in `Meta/AppBuilder.lean` +@[export pantograph_mk_fun_m] +def mkFun (constName : Name) : MetaM (Expr × Expr) := do + let cinfo ← getConstInfo constName + let us ← cinfo.levelParams.mapM fun _ => Meta.mkFreshLevelMVar + let f := mkConst constName us + let fType ← Meta.instantiateTypeLevelParams cinfo us + return (f, fType) @[export pantograph_expr_to_string] def exprToString (e: Expr): String := toString e