From 70c410eba2b2b0dc9bcaa7cc9164183d9d47b069 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 18 Nov 2013 21:29:48 -0800 Subject: [PATCH] doc(lua): add link to wikipedia splay tree page Signed-off-by: Leonardo de Moura --- doc/lua/lua.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/doc/lua/lua.md b/doc/lua/lua.md index 03c8c7dfc..073b4b843 100644 --- a/doc/lua/lua.md +++ b/doc/lua/lua.md @@ -99,7 +99,9 @@ assert(m[a] == 10) ## Splay maps In Lean, we provide splay maps for implementing mappings where the keys are -Lean objects such as hierarchical names. We can also use Lua atomic data types +Lean objects such as hierarchical names. A splay map is implemented using +a [splay tree](http://en.wikipedia.org/wiki/Splay_tree), a self-adjusting binary +search tree. We can also use Lua atomic data types as keys in splay maps. However, we should not mix different types in the same splay map. The Lean splay map assumes that `<` is a total order on the keys inserted in the map.