Pantograph/Environment.lean

@@ -148,7 +148,9 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): Protocol.
 def addDecl (name: String) (levels: Array String := #[]) (type: String) (value: String) (isTheorem: Bool)
     : Protocol.FallibleT CoreM Protocol.EnvAddResult := do
   let env ← Lean.MonadEnv.getEnv
-  let tvM: Elab.TermElabM (Except String (Expr × Expr)) := do
+  let levelParams := levels.toList.map (·.toName)
+  let tvM: Elab.TermElabM (Except String (Expr × Expr)) :=
+    Elab.Term.withLevelNames levelParams do do
     let type ← match parseTerm env type with
       | .ok syn => do
         match ← elabTerm syn with
@@ -164,11 +166,11 @@ def addDecl (name: String) (levels: Array String := #[]) (type: String) (value:
           pure $ expr
         catch ex => return .error (← ex.toMessageData.toString)
       | .error e => return .error e
-    pure $ .ok (type, value)
+    Elab.Term.synthesizeSyntheticMVarsNoPostponing
+    pure $ .ok (← instantiateMVars type, ← instantiateMVars value)
   let (type, value) ← match ← tvM.run' (ctx := {}) |>.run' with
     | .ok t => pure t
     | .error e => Protocol.throw $ Protocol.errorExpr e
-  let levelParams := levels.toList.map (·.toName)
   let decl := if isTheorem then
     Lean.Declaration.thmDecl <| Lean.mkTheoremValEx
       (name := name.toName)

Test/Integration.lean

@@ -162,6 +162,7 @@ def test_automatic_mode (automatic: Bool): Test :=
 def test_env_add_inspect : Test :=
   let name1 := "Pantograph.mystery"
   let name2 := "Pantograph.mystery2"
+  let name3 := "Pantograph.mystery3"
   [
     step "env.add"
       ({
@@ -190,9 +191,25 @@ def test_env_add_inspect : Test :=
        value? := .some { pp? := .some "fun a => ↑a + 1" },
        type := { pp? := .some "Nat → Int" },
      }:
-      Protocol.EnvInspectResult)
+      Protocol.EnvInspectResult),
+    step "env.add"
+      ({
+        name := name3,
+        levels := #["u"]
+        type := "(α : Type u) → α → (α × α)",
+        value := "λ (α : Type u) (x : α) => (x, x)",
+        isTheorem := false
+      }: Protocol.EnvAdd)
+     ({}: Protocol.EnvAddResult),
+    step "env.inspect" ({name := name3} : Protocol.EnvInspect)
+     ({
+       type := { pp? := .some "(α : Type u) → α → α × α" },
+     }:
+      Protocol.EnvInspectResult),
   ]
 
+def f.{u} : (α : Type u) → α → (α × α) := λ (α : Type u) (x : α) => (x, x)
+
 example : ∀ (p: Prop), p → p := by
   intro p h
   exact h