package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type ('constr, 'types) pt =
  1. | LocalAssum of Names.Name.t binder_annot * 'types
    (*

    name, type

    *)
  2. | LocalDef of Names.Name.t binder_annot * 'constr * 'types
    (*

    name, value, type

    *)
val get_annot : (_, _) pt -> Names.Name.t binder_annot
val get_name : ('c, 't) pt -> Names.Name.t

Return the name bound by a given declaration.

val get_value : ('c, 't) pt -> 'c option

Return Some value for local-declarations and None for local-assumptions.

val get_type : ('c, 't) pt -> 't

Return the type of the name bound by a given declaration.

val get_relevance : ('c, 't) pt -> Sorts.relevance
val set_name : Names.Name.t -> ('c, 't) pt -> ('c, 't) pt

Set the name that is bound by a given declaration.

val set_type : 't -> ('c, 't) pt -> ('c, 't) pt

Set the type of the bound variable in a given declaration.

val is_local_assum : ('c, 't) pt -> bool

Return true iff a given declaration is a local assumption.

val is_local_def : ('c, 't) pt -> bool

Return true iff a given declaration is a local definition.

val exists : ('c -> bool) -> ('c, 'c) pt -> bool

Check whether any term in a given declaration satisfies a given predicate.

val for_all : ('c -> bool) -> ('c, 'c) pt -> bool

Check whether all terms in a given declaration satisfy a given predicate.

val equal : ('c -> 'c -> bool) -> ('c, 'c) pt -> ('c, 'c) pt -> bool

Check whether the two given declarations are equal.

val map_name : (Names.Name.t -> Names.Name.t) -> ('c, 't) pt -> ('c, 't) pt

Map the name bound by a given declaration.

val map_value : ('c -> 'c) -> ('c, 't) pt -> ('c, 't) pt

For local assumptions, this function returns the original local assumptions. For local definitions, this function maps the value in the local definition.

val map_type : ('t -> 't) -> ('c, 't) pt -> ('c, 't) pt

Map the type of the name bound by a given declaration.

val map_constr : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt

Map all terms in a given declaration.

val map_constr_het : ('a -> 'b) -> ('a, 'a) pt -> ('b, 'b) pt

Map all terms, with an heterogeneous function.

val iter_constr : ('c -> unit) -> ('c, 'c) pt -> unit

Perform a given action on all terms in a given declaration.

val fold_constr : ('c -> 'a -> 'a) -> ('c, 'c) pt -> 'a -> 'a

Reduce all terms in a given declaration to a single value.

val to_tuple : ('c, 't) pt -> Names.Name.t binder_annot * 'c option * 't
val drop_body : ('c, 't) pt -> ('c, 't) pt

Turn LocalDef into LocalAssum, identity otherwise.

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