{-# OPTIONS --safe #-}
module Cubical.Data.Bool.SwitchStatement where
open import Cubical.Foundations.Prelude
open import Cubical.Data.Bool.Base
open import Cubical.Data.Nat
private
variable
ℓ ℓ' : Level
infixr 6 default⇒_
infixr 5 case_⇒_break_
infixr 4 switch_cases_
switch_cases_ : {A : Type ℓ} {B : Type ℓ'} → (A → Bool) → ((A → Bool) → B) → B
switch caseIndicator cases caseData = caseData caseIndicator
case_⇒_break_ : {A : Type ℓ} {B : Type ℓ'} → A → B → (otherCases : (A → Bool) → B) → (A → Bool) → B
case forValue ⇒ result break otherCases = λ caseIndicator → if (caseIndicator forValue) then result else (otherCases caseIndicator)
default⇒_ : {A : Type ℓ} {B : Type ℓ'} → B → (A → Bool) → B
default⇒_ value caseIndicator = value