package coq-core
Install
Dune Dependency
Authors
Maintainers
Sources
md5=0cfaa70f569be9494d24c829e6555d46
sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2
doc/coq-core.pretyping/Locus/index.html
Module Locus
Locus : positions in hypotheses and goals
Occurrences
type occurrences_expr = int or_var occurrences_gen
type 'a with_occurrences_expr = occurrences_expr * 'a
type occurrences = int occurrences_gen
type 'a with_occurrences = occurrences * 'a
Locations
Selecting the occurrences in body (if any), in type, or in both
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_expr * hyp_location_flag
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 =
| OnHyp of Names.Id.t * occurrences_expr * hyp_location_flag
| 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