diff --git a/tests/lean/run/pickle1.lean b/tests/lean/run/pickle1.lean new file mode 100644 index 000000000..60e72cbc0 --- /dev/null +++ b/tests/lean/run/pickle1.lean @@ -0,0 +1,7 @@ +import data.countable +open countable decidable bool prod list nat option +variable l : list (nat × bool) +check pickle l +eval pickle [2, 1] +example : unpickle (list nat) (pickle [1, 1]) = some [1, 1] := +rfl