package coq-core

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

Locus : positions in hypotheses and goals

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

    non-empty

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

    non-empty

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

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

type 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
type 'a hyp_location_expr = 'a with_occurrences * hyp_location_flag
type 'id clause_expr = {
  1. onhyps : 'id hyp_location_expr list option;
  2. concl_occs : occurrences_expr;
}
type clause = Names.Id.t clause_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

type 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

type 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

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

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

type simple_clause = Names.Id.t option list
A notion of occurrences allowing to express "all occurrences convertible to the first which matches"
type '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