package coq

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

Module Glob_opsSource

Sourceval map_glob_sort_gen : ('a -> 'b) -> 'a Glob_term.glob_sort_gen -> 'b Glob_term.glob_sort_gen

Equalities

Sourceval glob_sort_gen_eq : ('a -> 'a -> bool) -> 'a Glob_term.glob_sort_gen -> 'a Glob_term.glob_sort_gen -> bool
Sourceval glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool
Sourceval glob_level_eq : Glob_term.glob_level -> Glob_term.glob_level -> bool
Sourceval cases_pattern_eq : 'a Glob_term.cases_pattern_g -> 'a Glob_term.cases_pattern_g -> bool
Sourceexception ComplexSort

Expect a Prop/SProp/Set/Type universe; raise ComplexSort if contains a max, an increment, or a flexible universe

Sourceval glob_sort_family : Glob_term.glob_sort -> Sorts.family
Sourceval cast_type_eq : ('a -> 'a -> bool) -> 'a Glob_term.cast_type -> 'a Glob_term.cast_type -> bool
Sourceval glob_constr_eq : 'a Glob_term.glob_constr_g -> 'a Glob_term.glob_constr_g -> bool

Mapping cast_type

Sourceval map_cast_type : ('a -> 'b) -> 'a Glob_term.cast_type -> 'b Glob_term.cast_type
Sourceval smartmap_cast_type : ('a -> 'a) -> 'a Glob_term.cast_type -> 'a Glob_term.cast_type

Operations on glob_constr

Sourceval cases_pattern_loc : 'a Glob_term.cases_pattern_g -> Loc.t option
Sourceval cases_predicate_names : 'a Glob_term.tomatch_tuples_g -> Names.Name.t list

Apply a list of arguments to a glob_constr

Sourceval binding_kind_eq : Glob_term.binding_kind -> Glob_term.binding_kind -> bool

Equality on binding_kind

Ensure traversal from left to right

Sourceval warn_variable_collision : ?loc:Loc.t -> Names.Id.t -> unit
Sourceval fold_glob_constr : ('a -> Glob_term.glob_constr -> 'a) -> 'a -> Glob_term.glob_constr -> 'a
Sourceval fold_glob_constr_with_binders : (Names.Id.t -> 'a -> 'a) -> ('a -> 'b -> Glob_term.glob_constr -> 'b) -> 'a -> 'b -> Glob_term.glob_constr -> 'b
Sourceval iter_glob_constr : (Glob_term.glob_constr -> unit) -> Glob_term.glob_constr -> unit
Sourceval occur_glob_constr : Names.Id.t -> 'a Glob_term.glob_constr_g -> bool
Sourceval loc_of_glob_constr : 'a Glob_term.glob_constr_g -> Loc.t option
Sourceval glob_visible_short_qualid : 'a Glob_term.glob_constr_g -> Names.Id.Set.t
Sourceexception UnsoundRenaming
Sourceval rename_var : (Names.Id.t * Names.Id.t) list -> Names.Id.t -> Names.Id.t

map_pattern_binders f m c applies f to all the binding names in a pattern-matching expression (Glob_term.glob_constr_r.GCases) represented here by its relevant components m and c. It is used to interpret Ltac-bound names both in pretyping and printing of terms.

map_pattern f m c applies f to the return predicate and the right-hand side of a pattern-matching expression (Glob_term.glob_constr_r.GCases) represented here by its relevant components m and c.

Sourceval cases_pattern_of_glob_constr : Environ.env -> Names.Name.t -> 'a Glob_term.glob_constr_g -> 'a Glob_term.cases_pattern_g

Conversion from glob_constr to cases pattern, if possible

Evaluation is forced. Take the current alias as parameter,

  • raises Not_found

    if translation is impossible

Sourceval glob_constr_of_closed_cases_pattern : Environ.env -> 'a Glob_term.cases_pattern_g -> Names.Name.t * 'a Glob_term.glob_constr_g
Sourceval glob_constr_of_cases_pattern : Environ.env -> 'a Glob_term.cases_pattern_g -> 'a Glob_term.glob_constr_g

A canonical encoding of cases pattern into constr such that composed with cases_pattern_of_glob_constr Anonymous gives identity

Sourceval add_patterns_for_params_remove_local_defs : Environ.env -> Names.constructor -> 'a Glob_term.cases_pattern_g list -> 'a Glob_term.cases_pattern_g list
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