Function serialize_syntax_inner

crates/compile/src/compile.rs:1492–1524

(
  syn: &LeanSyntax,
  stt: &CompileState,
  bytes: &mut Vec<u8>,
)

                      stack.push(Frame::Compile(arg.clone()));
                    }
                    for arg in sorted_canon.iter().rev() {
                      stack.push(Frame::Compile(arg.clone()));
                    }
                    stack.push(Frame::Compile(head_expr.clone()));
                    continue;
                  }
                }
              }
            }

            // Normal telescope path: interleave BuildApp + Compile(arg) for
            // each arg (right to left), then Compile(head).
            // This compiles the same result as the recursive one-App-at-a-time
            // approach, but avoids re-entering the App branch for inner nodes.
            for &arg in args.iter().rev() {
              stack.push(Frame::BuildApp);
              stack.push(Frame::Compile(arg.clone()));
            }
            stack.push(Frame::Compile(head_expr.clone()));
          },

          ExprData::Lam(name, ty, body, info, _) => {
            let name_addr = compile_name(name, stt);
            stack.push(Frame::BuildLam(name_addr, info.clone()));
            stack.push(Frame::Compile(body.clone()));
            stack.push(Frame::Compile(ty.clone()));
          },

          ExprData::ForallE(name, ty, body, info, _) => {
            let name_addr = compile_name(name, stt);
            stack.push(Frame::BuildAll(name_addr, info.clone()));
            stack.push(Frame::Compile(body.clone()));
            stack.push(Frame::Compile(ty.clone()));
          },

          ExprData::LetE(name, ty, val, body, non_dep, _) => {