|
Dedekind 0.0.0
A structuralist C++23 Module Library
|
T's values are determined by its type, so a type-only lattice law (X∧X=X idempotence, a∧¬a=⊥ complement) collapses soundly on it: two same-type instances are necessarily the same value. A runtime-stateful leaf (say a Singleton holding a value, or a predicate with an expected field) is not idempotent, so those laws must not fire on it, else Meet{S{7},¬S{3}} would wrongly collapse to ⊥. This is the value-safety gate the type-level reducer shares with the value-first :lattice_term reducer (#922). Recursive over Meet / Join / Not through idempotent_leaf_v.
More...
T's values are determined by its type, so a type-only lattice law (X∧X=X idempotence, a∧¬a=⊥ complement) collapses soundly on it: two same-type instances are necessarily the same value. A runtime-stateful leaf (say a Singleton holding a value, or a predicate with an expected field) is not idempotent, so those laws must not fire on it, else Meet{S{7},¬S{3}} would wrongly collapse to ⊥. This is the value-safety gate the type-level reducer shares with the value-first :lattice_term reducer (#922). Recursive over Meet / Join / Not through idempotent_leaf_v.