From 1abd36dc0d31a26ce636fb89a5013b38826aa643 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 20 Jan 2021 18:13:56 -0800 Subject: [PATCH] test: `sizeOf` --- tests/lean/sizeof.lean | 9 +++++++++ tests/lean/sizeof.lean.expected.out | 8 ++++++++ 2 files changed, 17 insertions(+) create mode 100644 tests/lean/sizeof.lean create mode 100644 tests/lean/sizeof.lean.expected.out diff --git a/tests/lean/sizeof.lean b/tests/lean/sizeof.lean new file mode 100644 index 0000000000..c82d435774 --- /dev/null +++ b/tests/lean/sizeof.lean @@ -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 diff --git a/tests/lean/sizeof.lean.expected.out b/tests/lean/sizeof.lean.expected.out new file mode 100644 index 0000000000..085d8f45e8 --- /dev/null +++ b/tests/lean/sizeof.lean.expected.out @@ -0,0 +1,8 @@ +10 +6 +7 +12 +100 +553 +308 +310