source: Deliverables/D4.1/Matita/Map.ma @ 410

Last change on this file since 410 was 410, checked in by mulligan, 9 years ago

Using bitvectortries for a dictionary doesn't work even if we hypothesise conversion functions from bitvectors to string, and back again. Many changes, including most of the assembly function implemented.

File size: 636 bytes
Line 
1include "Universes.ma".
2include "Compare.ma".
3
4ninductive Map (A: Type[0]) (B: Type[0]): Type[0] ≝
5  Empty: Map A B
6| Leaf: A → B → Map A B
7| Node: A → B → Map A B → Map A B → Map A B.
8
9nlet rec insert (A: Type[0]) (B: Type[0])
10                (key: A) (f: A → A → Compare) (value: B) (map: Map A B) ≝
11  match map with
12    [ Empty ⇒ Leaf key value
13    | Leaf key' value' ⇒
14      match f key key' with
15        [ Equal ⇒ ?
16        | Less ⇒ ?
17        | Greater ⇒ ?
18        ]
19    | Node key' value' ⇒
20      match f key key' with
21        [ Equal ⇒ ?
22        | Less ⇒ ?
23        | Greater ?
24        ]
25    ].
Note: See TracBrowser for help on using the repository browser.