test: sizeOf

This commit is contained in:
Leonardo de Moura 2021-01-20 18:13:56 -08:00
parent e8401ea6e7
commit 1abd36dc0d
2 changed files with 17 additions and 0 deletions

9
tests/lean/sizeof.lean Normal file
View file

@ -0,0 +1,9 @@
-- Recall that we do not generate code for `sizeOf` instances since they are only used for proving termination
#reduce sizeOf 10
#reduce sizeOf [1, 2]
#reduce sizeOf #[1, 2]
#reduce sizeOf (10 : UInt8)
#reduce sizeOf 'a'
#reduce sizeOf ['h', 'e', 'l', 'l', 'o']
#reduce sizeOf "abc"
#reduce sizeOf `abc

View file

@ -0,0 +1,8 @@
10
6
7
12
100
553
308
310