let rec pp fmt s =
  Name.pp_map pp_entry fmt s
 
and pp_entry fmt e =
  let pr = Format.fprintf fmt in
  match e with
    | Def(Term(x)) -> pr "@[def("; Term.pp fmt x; pr ")@]"
    | Def(Prop(x)) -> pr "@[def("; Prop.pp fmt x; pr ")@]"
    | Arity(a) -> pr "@[sig("; Format.fprintf fmt "%d" a; pr ")@]"
    | Type(c) -> pr "@[type("; Dom.pp fmt c; pr ")@]"
    | State(s) -> 
        pr "@[state(";
        Pretty.set Atom.pp fmt (Atom.Set.elements (Context.ctxt_of s));
        pr ")@]"