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.