do
  let info ← Lean.MonadRef.mkInfoFromRefPos
  let scp ← Lean.getCurrMacroScope
  let quotCtx ← Lean.MonadQuotation.getContext
  pure
      {
        raw :=
          Lean.Syntax.node1 info `foo
            (Lean.Syntax.node1 info `token.a (Lean.Syntax.atom info "a")) } : ?m (Lean.TSyntax `foo)
fun x =>
  have __discr := x;
  if __discr.isOfKind `foo = true then
    have __discr_1 := __discr.getArg 0;
    if __discr_1.isOfKind `token.a = true then
      have __discr := __discr_1.getArg 0;
      true
    else
      have __discr := __discr.getArg 0;
      false
  else
    have __discr := x;
    false : Lean.Syntax → Bool