michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(tests/lean/interactive): adjust test to library reorg

Browse source
This commit is contained in:
Leonardo de Moura 2014-09-16 13:16:46 -07:00
parent 74cb289d48
commit 50f788a427
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/interactive/num2.lean
View file

@ -3,7 +3,7 @@
-- Released under Apache 2.0 license as described in the file LICENSE. -- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura -- 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. -- 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)))). -- The parser will generate the terms (pos (bit1 (bit1 (bit0 one)))), zero, and (pos (bit0 (bit1 (bit1 one)))).