43 type 'a bitVectorTrie =
45 | Node of Nat.nat * 'a bitVectorTrie * 'a bitVectorTrie
48 val bitVectorTrie_rect_Type4 :
49 ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
50 -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2
52 val bitVectorTrie_rect_Type3 :
53 ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
54 -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2
56 val bitVectorTrie_rect_Type2 :
57 ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
58 -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2
60 val bitVectorTrie_rect_Type1 :
61 ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
62 -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2
64 val bitVectorTrie_rect_Type0 :
65 ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
66 -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2
68 val bitVectorTrie_inv_rect_Type4 :
69 Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat -> 'a1
70 bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __ ->
71 'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2
73 val bitVectorTrie_inv_rect_Type3 :
74 Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat -> 'a1
75 bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __ ->
76 'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2
78 val bitVectorTrie_inv_rect_Type2 :
79 Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat -> 'a1
80 bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __ ->
81 'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2
83 val bitVectorTrie_inv_rect_Type1 :
84 Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat -> 'a1
85 bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __ ->
86 'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2
88 val bitVectorTrie_inv_rect_Type0 :
89 Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat -> 'a1
90 bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __ ->
91 'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2
93 val bitVectorTrie_discr :
94 Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> __
96 val bitVectorTrie_jmdiscr :
97 Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> __
100 Nat.nat -> (BitVector.bitVector -> 'a1 -> 'a2 -> 'a2) -> 'a1 bitVectorTrie
104 (BitVector.bitVector -> 'a1 -> 'a2 -> 'a2) -> 'a2 -> Nat.nat -> 'a1
105 bitVectorTrie -> BitVector.bitVector -> 'a2
108 Nat.nat -> BitVector.bitVector -> 'a1 bitVectorTrie -> 'a1 Types.option
110 val member : Nat.nat -> BitVector.bitVector -> 'a1 bitVectorTrie -> Bool.bool
113 Nat.nat -> BitVector.bitVector -> 'a1 bitVectorTrie -> 'a1 -> 'a1
115 val prepare_trie_for_insertion :
116 Nat.nat -> BitVector.bitVector -> 'a1 -> 'a1 bitVectorTrie
119 Nat.nat -> BitVector.bitVector -> 'a1 -> 'a1 bitVectorTrie -> 'a1
123 Nat.nat -> BitVector.bitVector -> 'a1 -> 'a1 bitVectorTrie -> 'a1
124 bitVectorTrie Types.option
127 Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie
131 type strong_decidable = (__, __) Types.sum
133 val strong_decidable_in_codomain :
134 Deqsets.deqSet -> Nat.nat -> __ bitVectorTrie -> __ -> strong_decidable