From c5403a970e326830a564bc740821d29d3c5886a5 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Sat, 12 Aug 2023 10:28:19 +0200 Subject: [PATCH] tweaks in bool.quox --- examples/bool.quox | 31 ++++++++++++++++--------------- 1 file changed, 16 insertions(+), 15 deletions(-) diff --git a/examples/bool.quox b/examples/bool.quox index 055e28f..7d3a065 100644 --- a/examples/bool.quox +++ b/examples/bool.quox @@ -1,34 +1,35 @@ -load "misc.quox"; +load "misc.quox" namespace bool { -def0 Bool : ★ = {true, false}; +def0 Bool : ★ = {true, false} def if-dep : 0.(P : Bool → ★) → (b : Bool) → ω.(P 'true) → ω.(P 'false) → P b = - λ P b t f ⇒ case b return b' ⇒ P b' of { 'true ⇒ t; 'false ⇒ f }; + λ P b t f ⇒ case b return b' ⇒ P b' of { 'true ⇒ t; 'false ⇒ f } -def if : 0.(A : ★) → (b : Bool) → ω.A → ω.A → A = - λ A ⇒ if-dep (λ _ ⇒ A); +def if : 0.(A : ★) → Bool → ω.A → ω.A → A = + λ A ⇒ if-dep (λ _ ⇒ A) def0 if-same : (A : ★) → (b : Bool) → (x : A) → if A b x x ≡ x : A = - λ A b x ⇒ if-dep (λ b' ⇒ if A b' x x ≡ x : A) b (δ _ ⇒ x) (δ _ ⇒ x); + λ A b x ⇒ if-dep (λ b' ⇒ if A b' x x ≡ x : A) b (δ _ ⇒ x) (δ _ ⇒ x) def if2 : 0.(A B : ★) → (b : Bool) → ω.A → ω.B → if¹ ★ b A B = - λ A B ⇒ if-dep (λ b ⇒ if-dep¹ (λ _ ⇒ ★) b A B); + λ A B ⇒ if-dep (λ b ⇒ if¹ ★ b A B) -def0 T : Bool → ★ = λ b ⇒ if¹ ★ b True False; +def0 T : Bool → ★ = λ b ⇒ if¹ ★ b True False -def boolω : Bool → [ω.Bool] = - λ b ⇒ if [ω.Bool] b ['true] ['false]; +def dup : Bool → [ω.Bool] = + λ b ⇒ if [ω.Bool] b ['true] ['false] -def true-not-false : Not ('true ≡ 'false : Bool) = - λ eq ⇒ coe (𝑖 ⇒ T (eq @𝑖)) 'true; +def0 true-not-false : Not ('true ≡ 'false : Bool) = + λ eq ⇒ coe (𝑖 ⇒ T (eq @𝑖)) 'true -- [todo] infix -def and : Bool → ω.Bool → Bool = λ a b ⇒ if Bool a b 'false; -def or : Bool → ω.Bool → Bool = λ a b ⇒ if Bool a 'true b; +def and : Bool → ω.Bool → Bool = λ a b ⇒ if Bool a b 'false +def or : Bool → ω.Bool → Bool = λ a b ⇒ if Bool a 'true b } -def0 Bool = bool.Bool; +def0 Bool = bool.Bool +def if = bool.if