From b6f251bcd33e3941cd653777068bd0bb2919a6a4 Mon Sep 17 00:00:00 2001
From: "E.W.Ayers" <edward.ayers@outlook.com>
Date: Sun, 19 Jun 2022 15:32:56 -0400
Subject: [PATCH] fix: SubExpr.Pos.toString not terminating

fixes 1232
---
 src/Lean/SubExpr.lean       | 2 +-
 tests/lean/run/subexpr.lean | 2 ++
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/Lean/SubExpr.lean b/src/Lean/SubExpr.lean
index a246e84b03..bf21f612e2 100644
--- a/src/Lean/SubExpr.lean
+++ b/src/Lean/SubExpr.lean
@@ -29,7 +29,7 @@ def root : Pos := (1 : Nat)
 
 instance : Inhabited Pos := ⟨root⟩
 
-def isRoot (p : Pos) : Bool := p.asNat == 1
+def isRoot (p : Pos) : Bool := p.asNat < maxChildren
 
 /-- The coordinate deepest in the Pos. -/
 def head (p : Pos) : Nat :=
diff --git a/tests/lean/run/subexpr.lean b/tests/lean/run/subexpr.lean
index 0f6de6d1cd..4b6848f3a9 100644
--- a/tests/lean/run/subexpr.lean
+++ b/tests/lean/run/subexpr.lean
@@ -17,3 +17,5 @@ theorem Pos.stringRoundtrip :
     let x := Pos.ofArray p
     some x == (Except.toOption $ Pos.fromString? $ Pos.toString $ x)
   ) := by native_decide
+
+#eval Pos.toString Nat.zero