Module `Name_abstraction.Make`

Parameters

module Bindable : Flambda2_nominal.Bindable.S

module Term : Flambda2_nominal.Name_abstraction.Term

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

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

include Flambda2_nominal.Contains_ids.S with type t := t

val ids_for_export : t -> Flambda2_nominal.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 -> Flambda2_nominal.Renaming.t -> t