Module `Named.Declaration`Source

Representation of local declarations.

Sourcetype ('constr, 'types, 'r) pt =

| LocalAssum of (Names.Id.t, 'r) pbinder_annot * 'types
(*
identifier, type
*)
| LocalDef of (Names.Id.t, 'r) pbinder_annot * 'constr * 'types
(*
identifier, value, type
*)

Sourceval get_annot : (_, _, 'r) pt -> (Names.Id.t, 'r) pbinder_annot

Sourceval get_id : ('c, 't, 'r) pt -> Names.Id.t

Return the identifier bound by a given declaration.

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

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

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

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

Sourceval get_relevance : ('c, 't, 'r) pt -> 'r

Sourceval set_id : Names.Id.t -> ('c, 't, 'r) pt -> ('c, 't, 'r) pt

Set the identifier that is bound by a given declaration.

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

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

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

Return true iff a given declaration is a local assumption.

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

Return true iff a given declaration is a local definition.

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

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

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

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

Source

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.

Sourceval map_id : (Names.Id.t -> Names.Id.t) -> ('c, 't, 'r) pt -> ('c, 't, 'r) pt

Map the identifier bound by a given declaration.

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

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

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

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

Map all terms in a given declaration.

Source

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

Map all terms in a given declaration.

Source

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

Map all terms, with an heterogeneous function.

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

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

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

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

Source

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

Source

val of_tuple : 
  ((Names.Id.t, 'r) pbinder_annot * 'c option * 't) ->
  ('c, 't, 'r) pt

Sourceval drop_body : ('c, 't, 'r) pt -> ('c, 't, 'r) pt

Turn LocalDef into LocalAssum, identity otherwise.

Source

val of_rel_decl : 
  (Names.Name.t -> Names.Id.t) ->
  ('c, 't, 'r) Rel.Declaration.pt ->
  ('c, 't, 'r) 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".

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

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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/rocq-runtime.kernel/Context/Named/Declaration/index.html

Module `Named.Declaration`Source

package rocq-runtime

Install

Dune Dependency

Authors

Maintainers

Sources

doc/rocq-runtime.kernel/Context/Named/Declaration/index.html

Module Named.DeclarationSource

Module `Named.Declaration`Source