package coq

  1. Overview
  2. Docs
package coq
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Constrexpr_opsSource

Constrexpr_ops: utilities on constr_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
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 error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a

For cases pattern parsing errors

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