From 193d94e7986fef4779f5ce171616a1bc3ad0d068 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 15 Jul 2024 11:42:02 -0700
Subject: [PATCH] feat: Expression creation and pretty printing

---
 Pantograph/Condensed.lean | 7 +++++++
 Pantograph/Library.lean   | 7 ++++---
 2 files changed, 11 insertions(+), 3 deletions(-)

diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean
index 57a8517..f6f4cdb 100644
--- a/Pantograph/Condensed.lean
+++ b/Pantograph/Condensed.lean
@@ -17,6 +17,13 @@ def nameToStr (s: String) : Name := s.toName
 @[export pantograph_name_is_inaccessible]
 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
+
+
 -- Mirrors Lean's LocalDecl
 structure LocalDecl where
   -- Default value is for testing
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index 8036103..eb34614 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -78,9 +78,10 @@ def createCoreState (imports: Array String): IO Core.State := do
     (trustLevel := 1)
   return { env := env }
 
-@[export pantograph_create_meta_context]
-def createMetaContext: IO Lean.Meta.Context := do
-  return {}
+@[export pantograph_meta_context]
+def metaContext: Lean.Meta.Context := {}
+@[export pantograph_meta_state]
+def metaState: Lean.Meta.State := {}
 
 @[export pantograph_env_catalog_m]
 def envCatalog: CoreM Protocol.EnvCatalogResult :=