length.v 653 Bytes
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2
From stdpp Require prelude strings list.

3
(** Check that we always get the [length] function on lists, not on strings. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36
Module test1.
  Import stdpp.base.
  Check length.
  Import stdpp.strings.
  Check length.
  Import stdpp.base.
  Check length.
End test1.

Module test2.
  Import stdpp.prelude.
  Check length.
  Import stdpp.strings.
  Check length.
  Import stdpp.prelude.
  Check length.
End test2.

Module test3.
  Import stdpp.strings.
  Check length.
  Import stdpp.prelude.
  Check length.
End test3.

Module test4.
  Import stdpp.list.
  Check length.
  Import stdpp.strings.
  Check length.
  Import stdpp.list.
  Check length.
End test4.