The β-reduction algebra: a leaf is its own normal form; a node is reduce_β over its reduced legs. reduce_β is a dependent call resolved by ADL against the node type, so a law lives next to its node: the composition unit law above is the canonical exhibit, and further node laws add their own overloads beside their vocabulary. No node carries an is-this-kind tag; dispatch is on the node type. More...

Public Member Functions
template<typename A>
constexpr A	operator() (const A &atom) const
template<typename N, typename... R> requires requires(const N& n, const R&... r) { reduce_β(n, r...); }
constexpr auto	operator() (const N &node, const R &... reduced) const

Detailed Description

The β-reduction algebra: a leaf is its own normal form; a node is reduce_β over its reduced legs. reduce_β is a dependent call resolved by ADL against the node type, so a law lives next to its node: the composition unit law above is the canonical exhibit, and further node laws add their own overloads beside their vocabulary. No node carries an is-this-kind tag; dispatch is on the node type.

The documentation for this struct was generated from the following file:

src/main/modules/dedekind/category/f_algebra.cppm

Public Member Functions

Detailed Description