ulkb.Theory.top

Theory.top = begin theory type_constructor bool 0 python_type_alias bool (𝔹 : *) BoolType type_constructor fun 2 right constant (equal : a → a → 𝔹) definition (true : 𝔹) ≔ (𝜆 p ⇒ p) = (𝜆 p ⇒ p) definition (and : 𝔹 → 𝔹 → 𝔹) ≔ 𝜆 p q ⇒ (𝜆 f ⇒ f p q) = (𝜆 f ⇒ f ⊤ ⊤) definition (implies : 𝔹 → 𝔹 → 𝔹) ≔ 𝜆 p q ⇒ p ∧ q ↔ p definition (forall : (a → 𝔹) → 𝔹) ≔ 𝜆 p ⇒ p = (𝜆 x ⇒ ⊤) definition (false : 𝔹) ≔ ∀ p, p definition (not : 𝔹 → 𝔹) ≔ 𝜆 p ⇒ p → ⊥ definition (or : 𝔹 → 𝔹 → 𝔹) ≔ 𝜆 p q ⇒ ∀ r, (p → r) → (q → r) → r definition (exists : (a → 𝔹) → 𝔹) ≔ 𝜆 p ⇒ ∀ q, (∀ x, p x → q) → q definition (exists1 : (a → 𝔹) → 𝔹) ≔ 𝜆 p ⇒ (exists p) ∧ (∀ x y, p x ∧ p y → x = y) type_constructor int 0 python_type_alias int (ℤ : *) IntType type_constructor real 0 python_type_alias float (ℝ : *) RealType type_constructor str 0 python_type_alias str (str : *) StrType end theory

The top theory.