Relations built at run time as terms: arrows \(A \rightsquigarrow B\) between products of carriers, their objects data (#1037). More...

#include <algorithm>
#include <array>
#include <concepts>
#include <cstddef>
#include <cstdint>
#include <initializer_list>
#include <limits>
#include <memory>
#include <optional>
#include <ranges>
#include <type_traits>
#include <utility>
#include <variant>
#include <vector>
import dedekind.sets;
import dedekind.relational:dyadic;
import dedekind.category;

Include dependency graph for rows.cppm:

Classes
struct	dedekind::relational::detail_rows::SortsSoFar
	The step of a ∧ over a row's cells: the next cell has the next column's sort. The fold's state is the verdict so far and the column reached. More...
struct	dedekind::relational::detail_rows::CellOfSort< Cs >
struct	dedekind::relational::Factor
	A factor of an object: a carrier (a leaf, its sort the column's), or the sum \(X + Y\) of two objects (#1039). A sum lays out a tag column (𝔹: which summand), then the left summand's columns, then the right's; a row reads only the active side, so every column keeps one carrier. More...
struct	dedekind::relational::detail_rows::AppendLeaf
	The step of a fold building the factors of a product of carriers: one leaf more. More...
struct	dedekind::relational::detail_rows::AppendColumns
	The step of the fold reading an object's columns off its factors: a leaf's sort; a sum's tag, then its summands' columns. More...
struct	dedekind::relational::Object
	An object: a product of factors in normal form, a list. The product is associative with unit `1` (the empty list), so \((A \times B) \times C\) and \(A \times (B \times C)\) are the same object by construction, and `>>` composes regardless of grouping. Read as a binary tree, (first, rest), where a tree is asked for (`kind` / `operands` in Python). The columns are its factors'. More...
struct	dedekind::relational::RelExpr< K, Cs >
	A relation \(A \rightsquigarrow B\) built at run time: a term over relations, its objects `dom` and `cod` data, its classifier a reading. More...
struct	dedekind::relational::RelExpr< K, Cs >::Member
struct	dedekind::relational::detail_rows::AsConstant< K >
	`as_constant` as a visitor over a row's cells. More...
struct	dedekind::relational::detail_rows::FirstSet< N >
	The step of a fold for the first index whose flag is set: the answer so far, or `N` while there is none. More...
struct	dedekind::relational::detail_rows::Identify< K >
	The step of the fold for `identified:` one equation more. More...
struct	dedekind::relational::detail_rows::Kept
	The step of the fold checking a projection's columns: each in `1` … `n` and none twice. `seen` has `n` + 1 slots. More...
struct	dedekind::relational::detail_rows::Keep
struct	dedekind::relational::detail_rows::Projected< K >
	The step of the fold building a projection: the next kept column's sort, and its equation `π_{n` + j} == `π_c`. More...
struct	dedekind::relational::detail_rows::Project< K >
struct	dedekind::relational::detail_rows::Ranges< K >
	A slot map by three ranges: the domain's columns, the codomain's, and the slots past the arity (a factor's own bound slots). More...
struct	dedekind::relational::detail_rows::AtDefault< K, Cs >
	The step of the fold for `at_defaults:` the column `i` at its sort's default. More...
struct	dedekind::relational::detail_rows::Encoded< K >
	The step of the fold for `encodes:` the predicate so far and the slot reached; a leaf moves one slot on, a sum asks that its tag pick a side and moves past its columns. More...
struct	dedekind::relational::detail_rows::EncodeFactor< K, Cs >
struct	dedekind::relational::detail_rows::BindMiddle< K >
	The step of the fold binding a composite's middle: the `i-th` from the innermost, `∃π_{n` + j} over the middle column `j` = `m` − `i`, so the outermost binds the first. More...
struct	dedekind::relational::detail_rows::WithSlot
	The step of the fold for `column_mask:` one slot's bit more. More...
struct	dedekind::relational::detail_rows::Defined< K >
	The columns [lo, hi) as defined by `p:` per column the term of a conjunct defining it over the columns of `others` alone, landing in the column's sort (a K₃ term defines no 𝔹 column), and whether nothing else is asked (the residual ⊤). Nothing where a column is not so defined. More...
struct	dedekind::relational::detail_rows::Defining< K >
	The step of the fold for `defined_columns:` the terms so far, the predicate left, and whether every column so far was defined. More...
struct	dedekind::relational::detail_rows::DefineColumn< K, Cs >
struct	dedekind::relational::LawSet< Re, W >
	The relations certified the law `W:` a datum on the universe of relations, so `𝔸<Re>{}` `&` `Total<Re>{}` is the set of total relations, membership its χ in K₃ (inferred, or not), and a map or an isomorphism a meet of such sets, nothing stored. Its χ obeys the facts the set is declared: closed under `>>`, so `S(f)` `∧` `S(g)` `≤` `S`(f `>>` `g`); a down-set or an up-set in ⊆; carried by `°` to its dagger law. Its complement is never inhabited by inference (`¬True`, else `Unknown`): Σ, not Π. More...

Concepts
concept	dedekind::relational::detail_rows::HasCarrierConstant
	The constant type `K` has its own hook for a carrier's value `c:` `carrier_constant`, found by argument-dependent lookup.

Typedefs
using	dedekind::relational::Columns = std::vector<std::size_t>
	The sorts of a row, one per column.
template<typename Re>
using	dedekind::relational::Total = LawSet<Re, Law::Total>
template<typename Re>
using	dedekind::relational::Univalent = LawSet<Re, Law::Univalent>
template<typename Re>
using	dedekind::relational::Injective = LawSet<Re, Law::Injective>
template<typename Re>
using	dedekind::relational::Surjective = LawSet<Re, Law::Surjective>

Functions
constexpr Columns	dedekind::relational::detail_rows::joined (Columns a, const Columns &b)
	`a` then `b:` the concatenation of two lists.
template<typename... Cs>
constexpr bool	dedekind::relational::of_columns (const dedekind::sets::Row< Cs... > &r, Columns cols)
	The row `r` has the columns `cols:` one cell per column, each of the column's sort, a fold over the cells.
constexpr bool	dedekind::relational::same_object (const Object &a, const Object &b)
template<std::ranges::input_range Sorts>
constexpr std::vector< Factor >	dedekind::relational::detail_rows::leaves (const Sorts &sorts)
	The leaves of these carriers, one each.
constexpr Columns	dedekind::relational::columns (const Object &o)
	The columns of an object: a fold over its factors, per factor a leaf's sort; a sum's tag, then its left summand's columns, then its right's.
constexpr Object	dedekind::relational::sum (const Object &x, const Object &y, std::size_t tag)
	The object \(X + Y\): one sum factor, its tag column of sort `tag` (the 𝔹 carrier's).
constexpr Object	dedekind::relational::operator* (const Object &a, const Object &b)
	The product \(A \times B\): the factors side by side (the normal form of an associative product).
template<typename K, typename... Cs>
constexpr RelExpr< K, Cs... >	dedekind::relational::operator& (const RelExpr< K, Cs... > &r, const dedekind::sets::Pred< K > &p)
	`R` `&` `p:` the former, the meet with the subobject `p` classifies (#826), every slot, constant and operator of `p` checked in its column's sort now.
template<typename K, typename... Cs>
RelExpr< K, Cs... >	dedekind::relational::operator\| (const RelExpr< K, Cs... > &, const dedekind::sets::Pred< K > &)=delete
	`R` \| `p:` refused; the filter is `R` `&` `p` (#826).
template<typename K, typename... Cs>
constexpr RelExpr< K, Cs... >	dedekind::relational::operator& (const RelExpr< K, Cs... > &a, const RelExpr< K, Cs... > &b)
	`R` `&` `S` and `R` \| `S` between the same objects: the lattice's nodes.
template<typename K, typename... Cs>
constexpr RelExpr< K, Cs... >	dedekind::relational::operator\| (const RelExpr< K, Cs... > &a, const RelExpr< K, Cs... > &b)
template<typename K, typename... Cs>
constexpr RelExpr< K, Cs... >	dedekind::relational::operator~ (const RelExpr< K, Cs... > &a)
	`~R`: the complement.
template<typename K, typename... Cs>
constexpr RelExpr< K, Cs... >	dedekind::relational::converse (const RelExpr< K, Cs... > &a)
	`R°:` the converse, \(B \rightsquigarrow A\), the dagger.
template<typename K, typename... Cs>
constexpr RelExpr< K, Cs... >	dedekind::relational::operator* (const RelExpr< K, Cs... > &a, const RelExpr< K, Cs... > &b)
	`R` `*` `S:` the tensor \(R \otimes S : A \times C \rightsquigarrow B \times D\). Two universes make the product universe (the universe over a product is the product of the universes).
template<typename K, typename... Cs>
constexpr RelExpr< K, Cs... >	dedekind::relational::operator>> (const RelExpr< K, Cs... > &a, const RelExpr< K, Cs... > &b)
	`R` `>>` `S:` Kleisli composition, \(R;S : A \rightsquigarrow C\) for \(R : A \rightsquigarrow B\) and \(S : B \rightsquigarrow C\), the ∃ over the whole middle object \(B\).
template<typename K, typename... Cs>
constexpr RelExpr< K, Cs... >	dedekind::relational::table (const RelExpr< K, Cs... > &r)
	\(A \rightsquigarrow B\) read as the table \(1 \rightsquigarrow A \times B\): every factor moved to the codomain. Rel is compact closed, \(A \times B \rightsquigarrow C \cong A \rightsquigarrow B \times C\), so the rows are the same; only `>>`, `*` and `converse` see where the factors sit. Whole factors move: a sum's columns stay together.
template<typename K, typename... Cs>
constexpr RelExpr< K, Cs... >	dedekind::relational::arrow (const RelExpr< K, Cs... > &r)
	A relation read as the arrow of all its factors but the last (the `Function`[A, …, B] convention): \(1 \rightsquigarrow A_1 \times \dots \times A_n\) as \(A_1 \times \dots \times A_{n-1} \rightsquigarrow A_n\). The same compact-closed iso as `table`, the other way.
template<typename K, typename C> requires HasCarrierConstant<K, C> \|\| std::constructible_from<K, const C&>
constexpr K	dedekind::relational::detail_rows::as_constant (const C &c)
	A carrier's value `c` as a constant of the grammar: the constant type's own hook beside it where it has one (`HasCarrierConstant`), else `K(c)`. A sum's tag and the defaults of its inactive side are written with it.
template<typename K, typename... Cs>
constexpr K	dedekind::relational::detail_rows::default_constant (std::size_t sort)
	The default of the sort `sort` as a constant: the representative a sum's inactive side holds.
template<typename... Cs>
constexpr std::size_t	dedekind::relational::detail_rows::tag_sort ()
	The sort of the 𝔹 carrier among the columns' carriers: a sum's tag.
template<typename K, typename... Cs>
constexpr RelExpr< K, Cs... >	dedekind::relational::sum (const RelExpr< K, Cs... > &a, const RelExpr< K, Cs... > &b)
	\(A + B\): the sum of two tables (sets), a table over the object \(X + Y\), its χ the copairing \([\chi_A, \chi_B]\) on the tag.
template<typename K>
constexpr dedekind::sets::Pred< K >	dedekind::relational::detail_rows::conjoined (const dedekind::sets::Pred< K > &p, const dedekind::sets::Pred< K > &q)
	`p` `∧` `q`, ⊤ the unit of ∧ (the one identity the readings apply).
template<typename K>
constexpr dedekind::sets::Pred< K >	dedekind::relational::detail_rows::identified (unsigned n, unsigned from, unsigned to, dedekind::sets::Pred< K > onto=dedekind::sets::Pred< K >::top())
	`∧_i` π_{from + i} == π_{to + i} over `n` columns: the equations identifying two copies of an object.
template<typename K, typename... Cs>
constexpr RelExpr< K, Cs... >	dedekind::relational::diag (const Object &obj)
	`η:` the identity \(\Delta_A = \{(x, x)\}\), the unit of `>>`.
template<typename K, typename... Cs>
constexpr RelExpr< K, Cs... >	dedekind::relational::copy (const Object &obj)
	`Copy:` \(A \rightsquigarrow A \times A\), \(x \mapsto (x, x)\), the comonoid of the Frobenius structure.
template<typename K, typename... Cs>
constexpr RelExpr< K, Cs... >	dedekind::relational::merge (const Object &obj)
	`Merge:` \(A \times A \rightsquigarrow A\), the converse of `copy`.
template<typename K, typename... Cs>
constexpr RelExpr< K, Cs... >	dedekind::relational::proj (const Object &obj, const std::vector< unsigned > &keep)
	The structural projection \(\pi : A \rightsquigarrow A[keep]\), the columns `keep` (1-based) of the object in that order.
template<typename K>
constexpr dedekind::sets::Pred< K >	dedekind::relational::detail_rows::tag_is (unsigned slot, bool b)
	`π_slot` == `b:` a sum's tag picks its side, ⊥ the left.
template<typename K, typename... Cs>
constexpr dedekind::sets::Pred< K >	dedekind::relational::detail_rows::at_defaults (const Object &o, unsigned first)
	The columns of `o` from the slot `first` + 1 on at their defaults: the inactive side of a sum.
template<typename K, typename... Cs>
constexpr dedekind::sets::Pred< K >	dedekind::relational::detail_rows::encodes (const Object &o, unsigned first)
	The columns of `o` from the slot `first` + 1 on encode a point of it: at each sum, the tag picks a side and the other holds its defaults, recursively. ⊤ for an object without sums. Every row of a product of leaves is a point; a row of a sum is one only so (a quantifier or a complement over the columns must not range over the others).
template<typename K, typename... Cs>
constexpr dedekind::sets::Pred< K >	dedekind::relational::predicate_of (const RelExpr< K, Cs... > &r)
	The predicate of a relation on the columns of its domain then its codomain, `π_1` … `π_n:` a reading of the term. A universe ⊤ (over a sum, the rows that encode a point: `encodes`); a former its predicate on its base's; the lattice nodes their connectives (a complement the negation normal form, ∃ and ∀ swapped); a converse its base's with the two objects' columns exchanged; a tensor the conjunction, the columns arranged domain, domain, codomain, codomain; a composite the ∃ over every column of the middle object (the monad's μ), outermost first. A quantifier binds the next slot past the columns, so a leg's own bound slots are renumbered with its columns and never captured.
template<typename K, typename... Cs>
constexpr dedekind::category::Ternary	dedekind::relational::verdict (const RelExpr< K, Cs... > &r, const typename RelExpr< K, Cs... >::Point &row)
	χ at a row of the columns, in K₃: the predicate reading with every quantifier an atom defines eliminated first (the fusion law), the rest searched within the relation's budget. The one χ: Python binds this.
constexpr unsigned	dedekind::relational::detail_rows::slot_bit (unsigned s)
	The bit of a slot in a mask, as `slots` spells it.
constexpr unsigned	dedekind::relational::detail_rows::column_mask (unsigned lo, unsigned hi)
	The mask of the slots [lo, hi).
template<typename K, typename... Cs>
constexpr std::optional< Defined< K > >	dedekind::relational::detail_rows::defined_columns (const dedekind::sets::Pred< K > &p, unsigned lo, unsigned hi, unsigned others, const Columns &cols, const dedekind::sets::Row< Cs... > &rep)
template<typename K, typename... Cs>
constexpr Laws	dedekind::relational::detail_rows::predicate_laws (const dedekind::sets::Pred< K > &p, unsigned nd, const Columns &cols, const dedekind::sets::Row< Cs... > &rep)
	The laws a comprehension certifies by the shape of its predicate: every codomain column defined by a term over the domain columns is univalence (at most one row above a point); with nothing else asked, totality too (an admitted operator is total on its carrier, so the term is a value at every point). Dually, the domain columns defined over the codomain's: injective, and surjective. `Δ` is all four; `copy` a map and injective; its converse `merge` univalent, injective and surjective.
template<typename K, typename... Cs>
constexpr Laws	dedekind::relational::detail_rows::laws_at (const RelExpr< K, Cs... > &r, unsigned nd)
	The laws of `r` read at the split `nd` (its first `nd` columns the domain): a leaf by its shape, a node by the engine (`node_laws`, :dyadic) on its legs' laws. The split belongs to the node being read: a lattice node's legs share its columns; an operation's facts hold at its own boundary, so ; `⊗` `+` and `°` read their legs at their own splits, and a root re-split by `arrow` or `table` is read by its shape.
template<typename K, typename... Cs>
constexpr Laws	dedekind::relational::laws (const RelExpr< K, Cs... > &r)
	The laws of a relation, inferred: a fold over the term reading the engine (`infer`, :dyadic) at each node, the leaves certified by their shape (`detail_rows::predicate_laws`), at the relation's own split of its columns into domain and codomain. `True` where a rule infers the law, `Unknown` where none does; the normal form may still decide the inclusion (`algebra`, `canonical`).
template<typename K, typename... Cs>
constexpr std::optional< std::vector< dedekind::sets::Term< K > > >	dedekind::relational::function_terms (const RelExpr< K, Cs... > &r, const dedekind::sets::Pred< K > &p)
	The value of a relation certified a map, as terms: per codomain column the term over the domain columns that defines it in `p`, when every codomain column is so defined and nothing else is asked (what makes a leaf total and univalent by its shape); nothing otherwise. What `ap(R, x)` evaluates.

Detailed Description

Relations built at run time as terms: arrows \(A \rightsquigarrow B\) between products of carriers, their objects data (#1037).

@partition :rows

Copyright: 2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.

rows__The_Term

A relation built at run time is an arrow \(R : A \rightsquigarrow B\) between two objects, each a product of carriers held as a flat list of sorts (a binary tree of products modulo associativity: the strict monoidal normal form, Mac Lane's coherence). Its points are rows of the columns of \(A\) then \(B\). It is a term whose nodes are the set grammar's and the relational calculus's:

node	typed twin	built by
`Universe`	`𝔸` over \(A \times B\)	`universe`
`Comprehension`	`Comprehension`, the one set former	`R` `&` `p`

Nothing n-ary is primitive: a table is a relation out of the unit, \(() \rightsquigarrow A_1 \times \dots \times A_n\), and a projection is composition with the structural relation proj. Nothing is flattened at construction: R & S is a Meet node over two relations. The classifier χ of a relation on its columns is a reading (a fold, predicate_of), as are its verdict and its written form; canonical (algebra) normalises the reading. Rewrites on the tree are the phase after this.

rows__The_Kleisli_Structure

A relation is the Kleisli arrow \(A \to \mathcal{P}B\) of the powerset monad, and the relational operations are the monad's:

monad	relation	here
\(\eta\), \(a \mapsto \{a\}\)	the identity \(\Delta_A\)	`diag`
Kleisli composition	the relative product \(R;S\)	`>>`
\(\mu\), the union	the \(\exists\) over the middle object

Pred::exists, one per middle column, in predicate_of(R >> S) |

The monad laws are decided by canonical where the ∃ eliminates: \(\Delta;R = R = R;\Delta\) and \((R;S);T = R;(S;T)\).

rows__The_Frobenius_Structure

Relations form a cartesian bicategory (category:cartesian_bicategory, #946): every object carries copy \(A \rightsquigarrow A \times A\) and merge, its converse, both relations here like any other, and \(R \wedge S = \mathrm{merge} \circ (R \otimes S) \circ \mathrm{copy}\). Composing along a product object is the general ∃ of >>, so the law is a test, decided by canonical once the middle is eliminated (a conjunction's operands are sorted, #884). The converse is the dagger: \((R;S)^\circ = S^\circ;R^\circ\), \(R^{\circ\circ} = R\).

Function Documentation

◆ copy()

template<typename K, typename... Cs>

RelExpr< K, Cs... > dedekind::relational::copy ( const Object & obj )

constexprexport

Copy: \(A \rightsquigarrow A \times A\), \(x \mapsto (x, x)\), the comonoid of the Frobenius structure.

Parameters

obj	the object.

◆ diag()

template<typename K, typename... Cs>

RelExpr< K, Cs... > dedekind::relational::diag ( const Object & obj )

constexprexport

η: the identity \(\Delta_A = \{(x, x)\}\), the unit of >>.

Parameters

obj	the object.

◆ function_terms()

template<typename K, typename... Cs>

std::optional< std::vector< dedekind::sets::Term< K > > > dedekind::relational::function_terms	(	const RelExpr< K, Cs... > &	r,
		const dedekind::sets::Pred< K > &	p )

constexprexport

The value of a relation certified a map, as terms: per codomain column the term over the domain columns that defines it in p, when every codomain column is so defined and nothing else is asked (what makes a leaf total and univalent by its shape); nothing otherwise. What ap(R, x) evaluates.

Parameters

r	the relation.
p	its predicate, pinned or with its quantifiers eliminated.

◆ joined()

Columns dedekind::relational::detail_rows::joined	(	Columns	a,
		const Columns &	b )

constexpr

a then b: the concatenation of two lists.

Parameters

a	the front.
b	the back.

◆ laws()

template<typename K, typename... Cs>

Laws dedekind::relational::laws ( const RelExpr< K, Cs... > & r )

constexprexport

The laws of a relation, inferred: a fold over the term reading the engine (infer, :dyadic) at each node, the leaves certified by their shape (detail_rows::predicate_laws), at the relation's own split of its columns into domain and codomain. True where a rule infers the law, Unknown where none does; the normal form may still decide the inclusion (algebra, canonical).

Parameters

r	the relation.

◆ leaves()

template<std::ranges::input_range Sorts>

std::vector< Factor > dedekind::relational::detail_rows::leaves ( const Sorts & sorts )

constexpr

The leaves of these carriers, one each.

Parameters

sorts the carriers.

◆ merge()

template<typename K, typename... Cs>

RelExpr< K, Cs... > dedekind::relational::merge ( const Object & obj )

constexprexport

Merge: \(A \times A \rightsquigarrow A\), the converse of copy.

Parameters

obj	the object.

◆ of_columns()

template<typename... Cs>

bool dedekind::relational::of_columns	(	const dedekind::sets::Row< Cs... > &	r,
		Columns	cols )

constexpr

The row r has the columns cols: one cell per column, each of the column's sort, a fold over the cells.

Template Parameters

Cs	the carriers.

Parameters

r	a row.
cols	the sorts.

◆ operator&() [1/2]

template<typename K, typename... Cs>

RelExpr< K, Cs... > dedekind::relational::operator&	(	const RelExpr< K, Cs... > &	a,
		const RelExpr< K, Cs... > &	b )

constexprexport

R & S and R | S between the same objects: the lattice's nodes.

Exceptions

not_admitted otherwise.

◆ operator&() [2/2]

template<typename K, typename... Cs>

RelExpr< K, Cs... > dedekind::relational::operator&	(	const RelExpr< K, Cs... > &	r,
		const dedekind::sets::Pred< K > &	p )

constexprexport

R & p: the former, the meet with the subobject p classifies (#826), every slot, constant and operator of p checked in its column's sort now.

Exceptions

not_admitted for a slot past the columns, or an operator not admitted.

◆ operator>>()

template<typename K, typename... Cs>

RelExpr< K, Cs... > dedekind::relational::operator>>	(	const RelExpr< K, Cs... > &	a,
		const RelExpr< K, Cs... > &	b )

constexprexport

R >> S: Kleisli composition, \(R;S : A \rightsquigarrow C\) for \(R : A \rightsquigarrow B\) and \(S : B \rightsquigarrow C\), the ∃ over the whole middle object \(B\).

Exceptions

not_admitted where R's codomain is not S's domain.

◆ predicate_laws()

template<typename K, typename... Cs>

Laws dedekind::relational::detail_rows::predicate_laws	(	const dedekind::sets::Pred< K > &	p,
		unsigned	nd,
		const Columns &	cols,
		const dedekind::sets::Row< Cs... > &	rep )

constexpr

The laws a comprehension certifies by the shape of its predicate: every codomain column defined by a term over the domain columns is univalence (at most one row above a point); with nothing else asked, totality too (an admitted operator is total on its carrier, so the term is a value at every point). Dually, the domain columns defined over the codomain's: injective, and surjective. Δ is all four; copy a map and injective; its converse merge univalent, injective and surjective.

Parameters

p	the predicate on the columns.
nd	the domain's columns.
cols	the sorts of all the columns.
rep	a row of them.

◆ proj()

template<typename K, typename... Cs>

RelExpr< K, Cs... > dedekind::relational::proj	(	const Object &	obj,
		const std::vector< unsigned > &	keep )

constexprexport

The structural projection \(\pi : A \rightsquigarrow A[keep]\), the columns keep (1-based) of the object in that order.

Exceptions

not_admitted on a repeated or absent column.

◆ sum() [1/2]

Object dedekind::relational::sum	(	const Object &	x,
		const Object &	y,
		std::size_t	tag )

constexprexport

The object \(X + Y\): one sum factor, its tag column of sort tag (the 𝔹 carrier's).

Parameters

x,y	the summands.

◆ sum() [2/2]

template<typename K, typename... Cs>

RelExpr< K, Cs... > dedekind::relational::sum	(	const RelExpr< K, Cs... > &	a,
		const RelExpr< K, Cs... > &	b )

constexprexport

\(A + B\): the sum of two tables (sets), a table over the object \(X + Y\), its χ the copairing \([\chi_A, \chi_B]\) on the tag.

Exceptions

not_admitted for a relation with a domain (a sum of arrows is not taken yet).

Classes

Concepts

Typedefs

Functions

Detailed Description

rows__The_Term

rows__The_Kleisli_Structure

rows__The_Frobenius_Structure

Function Documentation

◆ copy()

◆ diag()

◆ function_terms()

◆ joined()

◆ laws()

◆ leaves()

◆ merge()

◆ of_columns()

◆ operator&() [1/2]

◆ operator&() [2/2]

◆ operator>>()

◆ predicate_laws()

◆ proj()

◆ sum() [1/2]

◆ sum() [2/2]