fix name

lean-dojo · Sep 14, 2023 · 5fb59f4 · 5fb59f4
1 parent 9a4426d
commit 5fb59f4
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/lakefile.lean b/lakefile.lean
@@ -50,7 +50,7 @@ def getPlatform : IO SupportedPlatform := do
 syntax (name := isARM) "is_arm?" :term
 
 @[term_elab isARM]
-def elabGetConfig : TermElab := fun _ _ => do
+def elabIsARM : TermElab := fun _ _ => do
   if (← getArch) == .arm64 then
     return Expr.const `Bool.true []
   else