A slot's definition: the term t of a conjunct π_slot == t (or t == π_slot) with t free of the slot, and the conjunction without it. ∃π_slot. P is then the rest with t for π_slot: the existential is eliminated by substitution. Dually, under ∀ a disjunct π_slot != t defines it: ∀g. (g ≠ t ∨ Q) ≡ Q[t/g]. More...

Public Attributes
Term< K >	term
Pred< K >	rest

Detailed Description

template<typename K>
struct dedekind::sets::Definition< K >

A slot's definition: the term t of a conjunct π_slot == t (or t == π_slot) with t free of the slot, and the conjunction without it. ∃π_slot. P is then the rest with t for π_slot: the existential is eliminated by substitution. Dually, under ∀ a disjunct π_slot != t defines it: ∀g. (g ≠ t ∨ Q) ≡ Q[t/g].

Template Parameters

K	the constants' type.

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

src/main/modules/dedekind/sets/terms.cppm

Public Attributes

Detailed Description