File: numbers_import.v

package info (click to toggle)
coq-stdpp 1.11.0-1
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid, trixie
  • size: 1,696 kB
  • sloc: makefile: 52; sh: 35; sed: 1
file content (26 lines) | stat: -rw-r--r-- 401 bytes parent folder | download | duplicates (2) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
 
From stdpp Require base numbers prelude.

(** Check that we always get the [le] and [lt] functions on [nat]. *)
Module test1.
  Import stdpp.base.
  Check le.
  Check lt.
End test1.

Module test2.
  Import stdpp.prelude.
  Check le.
  Check lt.
End test2.

Module test3.
  Import stdpp.numbers.
  Check le.
  Check lt.
End test3.

Module test4.
  Import stdpp.list.
  Check le.
  Check lt.
End test4.