maonuGödel’s dialectica interpretation looks like pattern-match deconstruction—counter-“witness” (aka way to deal with, accept as an argument) to \( A \vee B \) is *both* a way to deal with A and a way to deal with B (after inspecting tags)
GNU social JP is a social network, courtesy of GNU social JP管理人. It runs on GNU social, version 2.0.2-dev, available under the GNU Affero General Public License.
All GNU social JP content and data are available under the Creative Commons Attribution 3.0 license.