equal
deleted
inserted
replaced
1 (*<*) |
1 (*<*) |
2 theory Trie = Main:; |
2 theory Trie imports Main begin; |
3 (*>*) |
3 (*>*) |
4 text{* |
4 text{* |
5 To minimize running time, each node of a trie should contain an array that maps |
5 To minimize running time, each node of a trie should contain an array that maps |
6 letters to subtries. We have chosen a |
6 letters to subtries. We have chosen a |
7 representation where the subtries are held in an association list, i.e.\ a |
7 representation where the subtries are held in an association list, i.e.\ a |