Module Rel.Declaration

type ('constr, 'types, 'r) pt =
| LocalAssum of (Names.Name.t, 'r) pbinder_annot * 'types(*

name, type

*)
| LocalDef of (Names.Name.t, 'r) pbinder_annot * 'constr * 'types(*

name, value, type

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

Return the name bound by a given declaration.

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

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

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

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

val get_relevance : ('c, 't, 'r) pt -> 'r
val set_annot : (Names.Name.t, 'r) pbinder_annot -> ('c, 't, 'r) pt -> ('c, 't, 'r) pt
val set_name : Names.Name.t -> ('c, 't, 'r) pt -> ('c, 't, 'r) pt

Set the name that is bound by a given declaration.

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

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

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

Return true iff a given declaration is a local assumption.

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

Return true iff a given declaration is a local definition.

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

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

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

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

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

Check whether the two given declarations are equal.

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

Map the name bound by a given declaration.

val map_relevance : ('r -> 'r) -> ('c, 't, 'r) pt -> ('c, 't, 'r) pt

Map the relevance

val map_value : ('c -> 'c) -> ('c, 't, 'r) pt -> ('c, 't, 'r) 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, 'r) pt -> ('c, 't, 'r) pt

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

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

Map all terms in a given declaration.

val map_constr_with_relevance : ('r -> 'r) -> ('c -> 'c) -> ('c, 'c, 'r) pt -> ('c, 'c, 'r) pt

Map all terms in a given declaration.

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

Map all terms, with an heterogeneous function.

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

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

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

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

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

Turn LocalDef into LocalAssum, identity otherwise.