Module Comp.SubgoalPath

type t =
  1. | Here
  2. | Intros of t
  3. | Suffices of exp * int * t
  4. | MetaSplit of exp * meta_branch_label * t
  5. | CompSplit of exp * Syncom.Id.cid_comp_const * t
  6. | ContextSplit of exp * context_case * t
val equals : 'a -> 'b -> 'c
type builder = t -> t
val start : 'a -> 'a
val append : builder -> builder -> builder
val build_here : builder -> t
val build_intros : t -> t
val build_suffices : exp -> int -> t -> t
val build_meta_split : exp -> meta_branch_label -> t -> t
val build_comp_split : exp -> Syncom.Id.cid_comp_const -> t -> t
val build_context_split : exp -> context_case -> t -> t