The arrow reading of logic negation ¬ = L::RFL on the truth object Ω — the canonical order-reversing arrow. More...

Public Types
using	Domain = typename L::Ω
using	Codomain = typename L::Ω

Public Member Functions
constexpr L::Ω	operator() (const typename L::Ω &a) const

Detailed Description

template<typename L>
struct dedekind::category::NegationArrow< L >

The arrow reading of logic negation ¬ = L::RFL on the truth object Ω — the canonical order-reversing arrow.

Where logic_complement is the op (used as RflOp in the op-trait bridge), NegationArrow carries the Domain / Codomain typedefs that make it an IsArrow, so :posetal can register it is_antimonotone_v: ¬ maps the truth chain to its reverse (on Boole, False<True becomes True>False; on Kleene the \(K_3\) chain reflects about Unknown), i.e. Op(a,b) ⇒ Op(¬b,¬a). It is the antitone mirror of Identity's monotone witness (#908). Being an involution (¬¬=id) it is morally an order-anti-isomorphism; the bijection certificate lives on :involution.

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

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

Public Types

Public Member Functions

Detailed Description