Module `Name_abstraction.Make`

Parameters

module Bindable : Bindable.S

module Term : Term

type nonrec t = (Bindable.t, Term.t) t

The type t is the equivalent of an atom abstraction construction "----" in nominal sets.

include Contains_ids.S with type t := t

val ids_for_export : t -> Ids_for_export.t

Gather all table identifiers to export them.

val create : Bindable.t -> Term.t -> t

val pattern_match : t -> f:(Bindable.t -> Term.t -> 'a) -> 'a

Concretion of an abstraction at a fresh name.

val pattern_match_for_printing : t -> f:(Bindable.t -> Term.t -> 'a) -> 'a

Like pattern_match, but only freshen if Flambda_features.freshen_when_printing is enabled.

val pattern_match_pair : 
  t ->
  t ->
  f:(Bindable.t -> Term.t -> Term.t -> 'a) ->
  'a

Concretion of a pair of abstractions at the same fresh name.

val (let<>) : t -> ((Bindable.t * Term.t) -> 'a) -> 'a

Same as pattern_match.

val apply_renaming : t -> Renaming.t -> t