quox/examples/bool.quox

29 lines
796 B
Text

load "misc.quox";
namespace bool {
def0 Bool : ★ = {true, false};
def boolω : 1.Bool → [ω.Bool] =
λ b ⇒ case1 b return [ω.Bool] of { 'true ⇒ ['true]; 'false ⇒ ['false] };
def if : 0.(A : ★) → 1.Bool → ω.A → ω.A → A =
λ A b t f ⇒ case1 b return A of { 'true ⇒ t; 'false ⇒ f };
-- [todo]: universe lifting
def0 If : 1.Bool → 0.★ → 0.★ → ★ =
λ b T F ⇒ case1 b return ★ of { 'true ⇒ T; 'false ⇒ F };
def0 T : ω.Bool → ★ = λ b ⇒ If b True False;
def true-not-false : Not ('true ≡ 'false : Bool) =
λ eq ⇒ coe (i ⇒ T (eq @i)) 'true;
-- [todo] infix
def and : 1.Bool → ω.Bool → Bool = λ a b ⇒ if Bool a b 'false;
def or : 1.Bool → ω.Bool → Bool = λ a b ⇒ if Bool a 'true b;
}
def0 Bool = bool.Bool;