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.
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.
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.
For local assumptions, this function returns the original local assumptions. For local definitions, this function maps the value in the local definition.
Map the type of the name bound by a given declaration.
Map all terms in a given declaration.
Map all terms in a given declaration.
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