Fix

Author: ajreynol

plugins/lean_meta/lean_meta_reduce.cpp

@@ -281,15 +281,15 @@ std::string LeanMetaReduce::getEmbedName(const Expr& oApp, MetaKind ctx)
                   << oApp;
   }
   const Literal* l = oApp[1].getValue()->asLiteral();
-  std::string smtStr = cleanSmtId(l->d_str.toString());
+  std::string smtStr = l->d_str.toString();
   // literals don't need native_
   if (is_integer(smtStr) || smtStr == "true" || smtStr == "false"
       || (!smtStr.empty() && smtStr.compare(0, 1, "\"") == 0))
   {
     return smtStr;
   }
   std::stringstream ss;
-  ss << "native_" << smtStr;
+  ss << "native_" << cleanSmtId(smtStr);
   return ss.str();
 }
 

plugins/lean_meta/lean_meta_spec.lean

@@ -36,7 +36,7 @@ Definitions for eo_is_obj
 noncomputable section
 
 def native_reserved_datatype_name (s : native_String) : native_Bool :=
-  s.startsWith "_at_"
+  s.startsWith "@"
 
 mutual
 

tools/eoc/out/lean/Spec.lean

@@ -38,7 +38,7 @@ Definitions for eo_is_obj
 noncomputable section
 
 def native_reserved_datatype_name (s : native_String) : native_Bool :=
-  s.startsWith "_at_"
+  s.startsWith "@"
 
 mutual