package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type

Utilities on or_var

val 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
type 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

val initialize_occurrence_counter : Locus.occurrences -> occurrences_count

Initialize an occurrence_counter

val update_occurrence_counter : occurrences_count -> bool * occurrences_count

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

val check_used_occurrences : occurrences_count -> unit

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

Auxiliary functions about occurrence counters

val current_occurrence : occurrences_count -> int

Tell the value of the current occurrence

val occurrences_done : occurrences_count -> bool

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

val 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
val is_selected : int -> Locus.occurrences -> bool
val is_all_occurrences : 'a Locus.occurrences_gen -> bool
val error_invalid_occurrence : int list -> 'a

Usual clauses

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

Tests

val is_nowhere : 'a Locus.clause_expr -> bool

Clause conversion functions, parametrized by a hyp enumeration function

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

Miscellaneous functions

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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct