{-# OPTIONS --cubical-compatible #-}
module Padova2025.ComputationalContent.DoubleNegation (⊥ : Set) where
Sarcastic interpretation of classical logic
Explain.
open import Padova2025.ProvingBasics.Connectives.Disjunction
infix 3 ¬_ ¬_ : Set → Set -- enter `¬` as `\neg` ¬ P = (P → ⊥)
return : {A : Set} → A → ¬ ¬ A return = {!!}
⊥-elim : {A : Set} → ⊥ → ¬ ¬ A ⊥-elim = {!!}
escape : ¬ ¬ ⊥ → ⊥ escape = {!!}
oracle : {A : Set} → ¬ ¬ (A ⊎ ¬ A) oracle = {!!}
infixl 1 _>>=_ _⟫=_
_>>=_ : {A B : Set} → ¬ ¬ A → (A → ¬ ¬ B) → ¬ ¬ B _>>=_ = {!!}
_⟫=_ : {A B : Set} → ¬ ¬ A → (A → ¬ ¬ B) → ¬ ¬ B _⟫=_ = _>>=_