From 5b3f6d97c5b1e6994a243e0b27e752e06e3e55ca Mon Sep 17 00:00:00 2001
From: memoryleak47 <memoryleak47@protonmail.ch>
Date: Mon, 6 Jan 2025 11:54:28 +0100
Subject: [PATCH] typo

---
 Lean/Egg/Core/Request/Synth.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Lean/Egg/Core/Request/Synth.lean b/Lean/Egg/Core/Request/Synth.lean
index 23ed6e9..81a8ac8 100644
--- a/Lean/Egg/Core/Request/Synth.lean
+++ b/Lean/Egg/Core/Request/Synth.lean
@@ -14,7 +14,7 @@ def parse (s: String) : MetaM Expr := do
 
   | .error _ => throwError "meh"
 
-@[export is_synthable]
+@[export lean_is_synthable]
 def isSynthable (ty : String) : MetaM Bool := do
   let ty_expr ← parse ty
   let opt ← Meta.synthInstance? ty_expr