source: driver/extracted/lists.mli @ 3106

Last change on this file since 3106 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 945 bytes
Line 
1open Preamble
2
3open Bool
4
5open Relations
6
7open Nat
8
9open Hints_declaration
10
11open Core_notation
12
13open Pts
14
15open Logic
16
17open Types
18
19open List
20
21open Div_and_mod
22
23open Jmeq
24
25open Russell
26
27open Util
28
29val all : ('a1 -> Bool.bool) -> 'a1 List.list -> Bool.bool
30
31val map_All : ('a1 -> __ -> 'a2) -> 'a1 List.list -> 'a2 List.list
32
33open Setoids
34
35open Monad
36
37open Option
38
39val append : 'a1 List.list List.aop
40
41val list : Monad.monadProps
42
43val count : ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat
44
45val position_of_safe : ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat
46
47val index_of : ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat
48
49val ordered_insert :
50  ('a1 -> 'a1 -> Bool.bool) -> 'a1 -> 'a1 List.list -> 'a1 List.list
51
52val insert_sort : ('a1 -> 'a1 -> Bool.bool) -> 'a1 List.list -> 'a1 List.list
53
54val range_strong_internal :
55  Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat Types.sig0 List.list
56
57val range_strong : Nat.nat -> Nat.nat Types.sig0 List.list
58
Note: See TracBrowser for help on using the repository browser.