package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

The Rocq Prover -- Core Binaries and Tools

Install

Dune Dependency

rocq-prover.org Readme Edit opam file Versions (1)

Authors

T

The Rocq development team, INRIA, CNRS, and contributors

Maintainers

T

The Rocq development team <coqdev@inria.fr>

Sources

rocq-9.0.0.tar.gz

md5=8d522602d23e7a665631826dab9aa92b

sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be

doc/rocq-runtime.pretyping/Locus/index.html

Module `Locus`

Locus : positions in hypotheses and goals

type 'a or_var =

| ArgArg of 'a
| ArgVar of Names.lident

Occurrences

type 'a occurrences_gen =

| AllOccurrences
| AtLeastOneOccurrence
| AllOccurrencesBut of 'a list
(*
non-empty
*)
| NoOccurrences
| OnlyOccurrences of 'a list
(*
non-empty
*)

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

type hyp_location_flag =

| InHyp
| InHypTypeOnly
| 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_expr * hyp_location_flag

type 'id clause_expr = {

onhyps : 'id hyp_location_expr list option;
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 =

| 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

A notion of occurrences allowing to express "all occurrences convertible to the first which matches"

type 'a or_like_first =

| AtOccs of 'a
| LikeFirst

On This Page

Occurrences
Locations
Abstract clauses expressions
Concrete view of occurrence clauses
A weaker form of clause with no mention of occurrences
Simple clauses, without occurrences nor location
A notion of occurrences allowing to express "all occurrences convertible to the first which matches"