package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.17.0.tar.gz
sha512=2f77bcb5211018b5d46320fd39fd34450eeb654aca44551b28bb50a2364398c4b34587630b6558db867ecfb63b246fd3e29dc2375f99967ff62bc002db9c3250

doc/coq-core.pretyping/Locus/index.html

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