Harpoon.Directive
type t =
| Intros of {
location : Beluga_syntax.Syncom.Location.t;
hypothetical : Hypothetical.t;
}
| Solve of {
location : Beluga_syntax.Syncom.Location.t;
solution : Synprs__.Synprs_definition.Comp.Expression_object.t;
}
| Split of {
location : Beluga_syntax.Syncom.Location.t;
scrutinee : Synprs__.Synprs_definition.Comp.Expression_object.t;
branches : Split_branch.t Support.List1.t;
}
| Impossible of {
location : Beluga_syntax.Syncom.Location.t;
scrutinee : Synprs__.Synprs_definition.Comp.Expression_object.t;
}
| Suffices of {
location : Beluga_syntax.Syncom.Location.t;
scrutinee : Synprs__.Synprs_definition.Comp.Expression_object.t;
branches : Suffices_branch.t Support.List.t;
}