Module Named.Declaration

Representation of local declarations.

type ('constr, 'types) pt =
| LocalAssum of Names.Id.t binder_annot * 'types(*

identifier, type

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

identifier, value, type

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

Return the identifier 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_id : Names.Id.t -> ( 'c, 't ) pt -> ( 'c, 't ) pt

Set the identifier 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_id : ( Names.Id.t -> Names.Id.t ) -> ( 'c, 't ) pt -> ( 'c, 't ) pt

Map the identifier 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.Id.t binder_annot * 'c option * 't
val of_tuple : (Names.Id.t binder_annot * 'c option * 't) -> ( 'c, 't ) pt
val drop_body : ( 'c, 't ) pt -> ( 'c, 't ) pt

Turn LocalDef into LocalAssum, identity otherwise.

val of_rel_decl : ( Names.Name.t -> Names.Id.t ) -> ( 'c, 't ) Rel.Declaration.pt -> ( 'c, 't ) pt

Convert Rel.Declaration.t value to the corresponding Named.Declaration.t value. The function provided as the first parameter determines how to translate "names" to "ids".

val to_rel_decl : ( 'c, 't ) pt -> ( 'c, 't ) Rel.Declaration.pt

Convert Named.Declaration.t value to the corresponding Rel.Declaration.t value.