fix: use Zero/One instead of HasZero/HasOne

leanprover-community · Nov 1, 2022 · a04dac6 · a04dac6
1 parent 6fffafa
commit a04dac6
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Mathport/Binary/Number.lean b/Mathport/Binary/Number.lean
@@ -31,13 +31,13 @@ structure NumInfo where
   deriving Inhabited
 
 partial def isNumber? (e : Expr) : Option NumInfo := do
-  if e.isAppOfArity `HasZero.zero 2 then pure {
+  if e.isAppOfArity `Zero.zero 2 then pure {
     number   := 0,
     level    := e.getAppFn.constLevels!.head!,
     type     := e.getArg! 0
     hasZero? := e.getArg! 1
   }
-  else if e.isAppOfArity `HasOne.one 2 then pure {
+  else if e.isAppOfArity `One.one 2 then pure {
     number  := 1,
     level   := e.getAppFn.constLevels!.head!,
     type    := e.getArg! 0,