Module `Locusops`Source

Utilities on or_var

Sourceval or_var_map : ('a -> 'b) -> 'a Locus.or_var -> 'b Locus.or_var

Utilities on occurrences

val occurrences_map : 
  ('a list -> 'b list) ->
  'a Locus.occurrences_gen ->
  'b Locus.occurrences_gen

Counting occurrences

Sourcetype occurrences_count

A counter of occurrences associated to a list of occurrences

Three basic functions to initialize, count, and conclude a loop browsing over subterms

Sourceval initialize_occurrence_counter : Locus.occurrences -> occurrences_count

Initialize an occurrence_counter

Sourceval update_occurrence_counter : occurrences_count -> bool * occurrences_count

Increase the occurrence counter by one and tell if the current occurrence is selected

Sourceval check_used_occurrences : occurrences_count -> unit

Increase the occurrence counter and tell if the current occurrence is selected

Auxiliary functions about occurrence counters

Sourceval current_occurrence : occurrences_count -> int

Tell the value of the current occurrence

Sourceval occurrences_done : occurrences_count -> bool

Tell if there are no more occurrences to select and if the loop can be shortcut

Sourceval more_specific_occurrences : occurrences_count -> bool

Tell if there are no more occurrences to select (or unselect) and if an inner loop can be shortcut

Miscellaneous

Sourceval is_selected : int -> Locus.occurrences -> bool

Sourceval is_all_occurrences : 'a Locus.occurrences_gen -> bool

Sourceval error_invalid_occurrence : int list -> 'a

Usual clauses

Sourceval allHypsAndConcl : 'a Locus.clause_expr

Sourceval allHyps : 'a Locus.clause_expr

Sourceval onConcl : 'a Locus.clause_expr

Sourceval nowhere : 'a Locus.clause_expr

Sourceval onHyp : 'a -> 'a Locus.clause_expr

Tests

Sourceval is_nowhere : 'a Locus.clause_expr -> bool

Clause conversion functions, parametrized by a hyp enumeration function

Source

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

Source

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

Miscellaneous functions

Source

val occurrences_of_hyp : 
  Names.Id.t ->
  Locus.clause ->
  Locus.occurrences * Locus.hyp_location_flag

Sourceval occurrences_of_goal : Locus.clause -> Locus.occurrences

Sourceval in_every_hyp : Locus.clause -> bool

Sourceval clause_with_generic_occurrences : 'a Locus.clause_expr -> bool

Sourceval clause_with_generic_context_selection : 'a Locus.clause_expr -> bool

Install

Dune Dependency

Authors

Maintainers

Sources

doc/rocq-runtime.pretyping/Locusops/index.html

Module `Locusops`Source

Counting occurrences

Miscellaneous

package rocq-runtime

Install

Dune Dependency

Authors

Maintainers

Sources

doc/rocq-runtime.pretyping/Locusops/index.html

Module LocusopsSource

Counting occurrences

Miscellaneous

Module `Locusops`Source