From e81f38c1167b04be7421074ea99bb6da26688acf Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 24 Nov 2019 08:17:44 -0800
Subject: [PATCH] doc: add comment about representation

---
 src/Init/Lean/Meta/DiscrTree.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Init/Lean/Meta/DiscrTree.lean b/src/Init/Lean/Meta/DiscrTree.lean
index 6b585a74fb..1a816092db 100644
--- a/src/Init/Lean/Meta/DiscrTree.lean
+++ b/src/Init/Lean/Meta/DiscrTree.lean
@@ -13,6 +13,9 @@ namespace DiscrTree
 
 /-
   (Imperfect) discrimination trees.
+  We use a hybrid representation.
+  - A `PersistentHashMap` for the root node which usually contains many children.
+  - A sorted array of key/node pairs for inner nodes.
 
   The edges are labeled by keys:
   - Constant names (and arity). Universe levels are ignored.