package coq

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

Module Rel.DeclarationSource

Sourcetype ('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

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

Return the name bound by a given declaration.

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

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

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

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

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

Set the name that is bound by a given declaration.

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

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

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

Return true iff a given declaration is a local assumption.

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

Return true iff a given declaration is a local definition.

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

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

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

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

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

Check whether the two given declarations are equal.

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

Map the name bound by a given declaration.

Sourceval 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.

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

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

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

Map all terms in a given declaration.

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

Map all terms, with an heterogeneous function.

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

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

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

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

Sourceval to_tuple : ('c, 't) pt -> Names.Name.t binder_annot * 'c option * 't
Sourceval 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