package coq

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

Module LocusSource

Locus : positions in hypotheses and goals

Sourcetype 'a or_var =
  1. | ArgArg of 'a
  2. | ArgVar of Names.lident
Occurrences
Sourcetype 'a occurrences_gen =
  1. | AllOccurrences
  2. | AtLeastOneOccurrence
  3. | AllOccurrencesBut of 'a list
    (*

    non-empty

    *)
  4. | NoOccurrences
  5. | OnlyOccurrences of 'a list
    (*

    non-empty

    *)
Sourcetype occurrences_expr = int or_var occurrences_gen
Sourcetype 'a with_occurrences = occurrences_expr * 'a
Sourcetype occurrences = int occurrences_gen
Locations

Selecting the occurrences in body (if any), in type, or in both

Sourcetype hyp_location_flag =
  1. | InHyp
  2. | InHypTypeOnly
  3. | InHypValueOnly
Abstract clauses expressions

A clause_expr (and its instance clause) denotes occurrences and hypotheses in a goal in an abstract way; in particular, it can refer to the set of all hypotheses independently of the effective contents of the current goal

Concerning the field onhyps:

  • None means *on every hypothesis*
  • Some l means on hypothesis belonging to l
Sourcetype 'a hyp_location_expr = 'a with_occurrences * hyp_location_flag
Sourcetype 'id clause_expr = {
  1. onhyps : 'id hyp_location_expr list option;
  2. concl_occs : occurrences_expr;
}
Concrete view of occurrence clauses

clause_atom refers either to an hypothesis location (i.e. an hypothesis with occurrences and a position, in body if any, in type or in both) or to some occurrences of the conclusion

Sourcetype clause_atom =
  1. | OnHyp of Names.Id.t * occurrences_expr * hyp_location_flag
  2. | OnConcl of occurrences_expr

A concrete_clause is an effective collection of occurrences in the hypotheses and the conclusion

Sourcetype concrete_clause = clause_atom list
A weaker form of clause with no mention of occurrences

A hyp_location is an hypothesis together with a location

Sourcetype hyp_location = Names.Id.t * hyp_location_flag

A goal_location is either an hypothesis (together with a location) or the conclusion (represented by None)

Sourcetype goal_location = hyp_location option
Simple clauses, without occurrences nor location

A simple_clause is a set of hypotheses, possibly extended with the conclusion (conclusion is represented by None)

Sourcetype simple_clause = Names.Id.t option list
A notion of occurrences allowing to express "all occurrences convertible to the first which matches"
Sourcetype 'a or_like_first =
  1. | AtOccs of 'a
  2. | LikeFirst
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