package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

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

Authors

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

Maintainers

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

Sources

rocq-9.0.0.tar.gz
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be

doc/rocq-runtime.interp/Constrexpr_ops/index.html

Module Constrexpr_opsSource

Constrexpr_ops: utilities on constr_expr

Sourceval expr_Type_sort : Constrexpr.sort_expr
Sourceval expr_SProp_sort : Constrexpr.sort_expr
Sourceval expr_Prop_sort : Constrexpr.sort_expr
Sourceval expr_Set_sort : Constrexpr.sort_expr
Sourceval sort_expr_eq : Constrexpr.sort_expr -> Constrexpr.sort_expr -> bool

Equality on explicitation.

Equality on constr_expr. This is a syntactical one, which is oblivious to some parsing details, including locations.

Equality on local_binder_expr. Same properties as constr_expr_eq.

Equality on binder_kind

Retrieving locations
Sourceval constr_loc : Constrexpr.constr_expr -> Loc.t option
Sourceval cases_pattern_expr_loc : Constrexpr.cases_pattern_expr -> Loc.t option
Sourceval local_binders_loc : Constrexpr.local_binder_expr list -> Loc.t option
Constructors
Term constructors

Basic form of the corresponding constructors

Basic form of application, collapsing nested applications

Optimized constructors: does not add a constructor for an empty binder list

Aliases for the corresponding constructors; generally mkLambdaCN and mkProdCN should be preferred

Pattern constructors

Interpretation of a list of patterns as a disjunctive pattern (optimized)

Apply a list of pattern arguments to a pattern

Destructors
Sourceval coerce_reference_to_id : Libnames.qualid -> Names.Id.t

FIXME: nothing to do here

Destruct terms of the form CRef (Ident _).

Destruct terms of the form CRef (Ident _) or CHole _.

Sourceval coerce_to_cases_pattern_expr : Constrexpr.constr_expr -> Constrexpr.cases_pattern_expr
Binder manipulation
Sourceval default_binder_kind : Constrexpr.binder_kind
Sourceval names_of_local_binders : Constrexpr.local_binder_expr list -> Names.lname list

Retrieve a list of binding names from a list of binders.

Sourceval names_of_local_assums : Constrexpr.local_binder_expr list -> Names.lname list

Same as names_of_local_binder_exprs, but does not take the let bindings into account.

Folds and maps
Sourceval fold_constr_expr_with_binders : (Names.Id.t -> 'a -> 'a) -> ('a -> 'b -> Constrexpr.constr_expr -> 'b) -> 'a -> 'b -> Constrexpr.constr_expr -> 'b

Used in typeclasses

Used in correctness and interface; absence of var capture not guaranteed in pattern-matching clauses and in binders of the form x,y:T(x)

Sourceval map_constr_expr_with_binders : (Names.Id.t -> 'a -> 'a) -> ('a -> Constrexpr.constr_expr -> Constrexpr.constr_expr) -> 'a -> Constrexpr.constr_expr -> Constrexpr.constr_expr
Miscellaneous
Sourceval free_vars_of_constr_expr : Constrexpr.constr_expr -> Names.Id.Set.t
Sourceval occur_var_constr_expr : Names.Id.t -> Constrexpr.constr_expr -> bool
Sourceval names_of_constr_expr : Constrexpr.constr_expr -> Names.Id.Set.t

Return all (non-qualified) names treating binders as names

Sourceval ntn_loc : ?loc:Loc.t -> Constrexpr.constr_notation_substitution -> Constrexpr.notation -> (int * int) list
Sourceval isCSort : Constrexpr.constr_expr -> bool
Sourceval error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a

For cases pattern parsing errors