package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

Constrexpr_ops: utilities on constr_expr

val sort_name_expr_eq : Constrexpr.sort_name_expr -> Constrexpr.sort_name_expr -> bool
val univ_level_expr_eq : Constrexpr.univ_level_expr -> Constrexpr.univ_level_expr -> bool
val sort_expr_eq : Constrexpr.sort_expr -> Constrexpr.sort_expr -> bool
val explicitation_eq : Constrexpr.explicitation -> Constrexpr.explicitation -> bool

Equality on explicitation.

val constr_expr_eq : Constrexpr.constr_expr -> Constrexpr.constr_expr -> bool

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.

val binder_kind_eq : Constrexpr.binder_kind -> Constrexpr.binder_kind -> bool

Equality on binder_kind

Retrieving locations
val constr_loc : Constrexpr.constr_expr -> Loc.t option
val cases_pattern_expr_loc : Constrexpr.cases_pattern_expr -> Loc.t option
val 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
val coerce_reference_to_id : Libnames.qualid -> Names.Id.t

FIXME: nothing to do here

val coerce_to_id : Constrexpr.constr_expr -> Names.lident

Destruct terms of the form CRef (Ident _).

val coerce_to_name : Constrexpr.constr_expr -> Names.lname

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

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

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

val 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
val 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)

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

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

val ntn_loc : ?loc:Loc.t -> Constrexpr.constr_notation_substitution -> Constrexpr.notation -> (int * int) list
val patntn_loc : ?loc:Loc.t -> Constrexpr.cases_pattern_notation_substitution -> Constrexpr.notation -> (int * int) list
val 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