diff --git a/src/Lean/Meta/DiscrTree/Util.lean b/src/Lean/Meta/DiscrTree/Util.lean
index 8b56d1360c40..bd95cbfc7162 100644
--- a/src/Lean/Meta/DiscrTree/Util.lean
+++ b/src/Lean/Meta/DiscrTree/Util.lean
@@ -51,7 +51,37 @@ partial def size : Trie α → Nat
     children.foldl (init := vs.size) fun n (_, c) => n + size c
 
 /--
-Checks that a trie node has no values and no children.
+Generate a trie node from values and an array of children.
+-/
+@[inline]
+def mkNode (vs : Array α) (cs : Array (Key × Trie α)) : Trie α :=
+  .node vs cs
+
+/--
+Inspect a trie node as an array of values and an array of children.
+-/
+@[inline]
+def asNode : Trie α → Array α × Array (Key × Trie α)
+  | .node vs cs => ⟨vs, cs⟩
+
+/--
+Returns the values stored at the current trie node.
+Equivalent to `t.asNode.1`.
+-/
+@[inline]
+def nodeValues : Trie α → Array α
+  | .node vs _ => vs
+
+/--
+Returns the child nodes of the current trie node.
+Equivalent to `t.asNode.2`.
+-/
+@[inline]
+def nodeChildren : Trie α → Array (Key × Trie α)
+  | .node _ cs => cs
+
+/--
+Checks whether a trie node is empty (no values and no children).
 
 This is only a check for actual trie emptiness (`t.size = 0`) if all operations maintain the
 invariant that no trie node has an empty child node.