From eb65cbdb4699e7c34c8e47c98e70f1a7a51e2420 Mon Sep 17 00:00:00 2001
From: Aletheia-Prime <221768278+Aletheia-Prime@users.noreply.github.com>
Date: Sat, 11 Apr 2026 01:25:22 -0300
Subject: [PATCH] Fix children iterators to include Def variants (Issue #719)

The children iterators in Term were incorrectly not returning the 'nxt' field from Def variants.
This caused AST traversal passes to miss subtrees, leading to various compilation bugs.

This adds proper handling for Def terms in both children() and children_mut() methods.
---
 src/fun/mod.rs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/fun/mod.rs b/src/fun/mod.rs
index a4ad06e6..698a7278 100644
--- a/src/fun/mod.rs
+++ b/src/fun/mod.rs
@@ -599,13 +599,13 @@ impl Term {
       Term::Lam { bod, .. } | Term::With { bod, .. } | Term::Open { bod, .. } => {
         ChildrenIter::One([bod.as_ref()])
       }
+      Term::Def { def: _, nxt } => ChildrenIter::One([nxt.as_ref()]),
       Term::Var { .. }
       | Term::Link { .. }
       | Term::Num { .. }
       | Term::Nat { .. }
       | Term::Str { .. }
       | Term::Ref { .. }
-      | Term::Def { .. }
       | Term::Era
       | Term::Err => ChildrenIter::Zero([]),
     }
@@ -635,13 +635,13 @@ impl Term {
       Term::Lam { bod, .. } | Term::With { bod, .. } | Term::Open { bod, .. } => {
         ChildrenIter::One([bod.as_mut()])
       }
+      Term::Def { def: _, nxt } => ChildrenIter::One([nxt.as_mut()]),
       Term::Var { .. }
       | Term::Link { .. }
       | Term::Num { .. }
       | Term::Nat { .. }
       | Term::Str { .. }
       | Term::Ref { .. }
-      | Term::Def { .. }
       | Term::Era
       | Term::Err => ChildrenIter::Zero([]),
     }