diff --git a/tests/lean/interactive/num2.lean b/tests/lean/interactive/num2.lean index 5a3b2b242..b5b38d6d5 100644 --- a/tests/lean/interactive/num2.lean +++ b/tests/lean/interactive/num2.lean @@ -3,7 +3,7 @@ -- Released under Apache 2.0 license as described in the file LICENSE. -- Author: Leonardo de Moura ---------------------------------------------------------------------------------------------------- -import logic.classes.inhabited +import logic.core.inhabited -- pos_num and num are two auxiliary datatypes used when parsing numerals such as 13, 0, 26. -- The parser will generate the terms (pos (bit1 (bit1 (bit0 one)))), zero, and (pos (bit0 (bit1 (bit1 one)))).