def get_tactic_state(dp, sep="\t"):
    """
    Args:
      dp: LeanStepDatapoint in JSON format. The specification of this format is given by the
          `has_to_tactic_json` instance in `./src/data_util/lean_step.lean`

    Returns:
      A formatted tactic state.
    """
    hyps_strings_state = []
    last_tp = None
    for nm, tp in dp["hyps"]:
        if not last_tp == tp:
            hyps_strings_state.append(([nm], tp))
            last_tp = tp
        else:
            hyps_strings_state[-1][0].append(nm)

    hyps_strings = []
    n_hyps = len(hyps_strings_state)
    for i, (nms, tp) in enumerate(hyps_strings_state):
        hyps_strings.append(" ".join(nms) + " : " + tp + ("," if i < n_hyps - 1 else ""))

    goal = dp["goal"]
    goal_string = f"⊢ {goal}"
    return sep.join(hyps_strings + [goal_string])
    # hyps_strings_state = collections.defaultdict(list)
    # for nm, tp in dp["hyps"]:
    #     hyps_strings_state[tp].append(nm)
    # n_hyps = len(hyps_strings_state)
    # hyps_strings = []
    # for i, (tp, nms) in enumerate(hyps_strings_state.items()):
    #     hyps_strings.append(" ".join(nms) + " : " + tp + ("," if i < n_hyps-1 else ""))
    # goal = dp["goal"]
    # goal_string = f"⊢ {goal}"
    # return sep.join(hyps_strings + [goal_string])