Module `Locusops`

Utilities on occurrences

val occurrences_map : ('a list -> 'b list) -> 'a Locus.occurrences_gen -> 'b Locus.occurrences_gen
val convert_occs : Locus.occurrences -> bool * int list: From occurrences to a list of positions (or complement of positions)

val is_selected : int -> Locus.occurrences -> bool
val is_all_occurrences : 'a Locus.occurrences_gen -> bool

val allHypsAndConcl : 'a Locus.clause_expr
val allHyps : 'a Locus.clause_expr
val onConcl : 'a Locus.clause_expr
val nowhere : 'a Locus.clause_expr
val onHyp : 'a -> 'a Locus.clause_expr

val is_nowhere : 'a Locus.clause_expr -> bool

val simple_clause_of : (unit -> Names.Id.t list) -> Locus.clause -> Locus.simple_clause
val concrete_clause_of : (unit -> Names.Id.t list) -> Locus.clause -> Locus.concrete_clause

val occurrences_of_hyp : Names.Id.t -> Locus.clause -> Locus.occurrences * Locus.hyp_location_flag
val occurrences_of_goal : Locus.clause -> Locus.occurrences
val in_every_hyp : Locus.clause -> bool
val clause_with_generic_occurrences : 'a Locus.clause_expr -> bool
val clause_with_generic_context_selection : 'a Locus.clause_expr -> bool