From 0bc7bc58565cceb839c41a11d207e4eeb64a845e Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 14 Aug 2024 01:20:56 -0700
Subject: [PATCH] refactor: Remove export of Lean functions

If the user wishes to use Lean functions, they should add the bindings manually.
---
 Pantograph/Condensed.lean | 42 ---------------------------------------
 flake.nix                 |  4 +---
 2 files changed, 1 insertion(+), 45 deletions(-)

diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean
index 8696523..c47f882 100644
--- a/Pantograph/Condensed.lean
+++ b/Pantograph/Condensed.lean
@@ -9,39 +9,6 @@ open Lean
 namespace Pantograph
 namespace Condensed
 
-/-
-These two functions are for user defiend names. For internal names such as
-`_uniq`, it is favourable to use `lean_name_hash_exported` and `lean_name_eq` to
-construct hash maps for Lean names.
--/
-@[export pantograph_str_to_name]
-def strToName (s: String) : Name := s.toName
-@[export pantograph_name_to_str]
-def nameToStr (s: Name) : String := s.toString
-@[export pantograph_name_is_inaccessible]
-def isInaccessible (n: Name) : Bool := n.isInaccessibleUserName || n.hasMacroScopes
-
-@[export pantograph_mk_app_m]
-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
-@[export pantograph_pp_expr_m]
-def ppExpr (e: Expr): MetaM String := toString <$> Meta.ppExpr e
-@[export pantograph_get_used_constants]
-def getUsedConstants (e: Expr) := e.getUsedConstants
-
-
 -- Mirrors Lean's LocalDecl
 structure LocalDecl where
   -- Default value is for testing
@@ -61,20 +28,11 @@ structure Goal where
 @[export pantograph_goal_is_lhs]
 def isLHS (g: Goal) : Bool := isLHSGoal? g.target |>.isSome
 
-
 -- Functions for creating contexts and states
-@[export pantograph_meta_context]
-def metaContext: Meta.Context := {}
-@[export pantograph_meta_state]
-def metaState: Meta.State := {}
 @[export pantograph_elab_context]
 def elabContext: Elab.Term.Context := {
     errToSorry := false
   }
-@[export pantograph_elab_state]
-def elabState (levelNames: Array Name): Elab.Term.State := {
-    levelNames := levelNames.toList,
-  }
 
 end Condensed
 
diff --git a/flake.nix b/flake.nix
index 2b68c0c..54a139f 100644
--- a/flake.nix
+++ b/flake.nix
@@ -63,10 +63,8 @@
       packages = {
         inherit (leanPkgs) lean lean-all;
         inherit (project) sharedLib executable;
-        default = project.executable;
-      };
-      dependencies = {
         inherit project leanPkgs;
+        default = project.executable;
       };
       checks = {
         test = pkgs.runCommand "test" {