UniAgda.Core.Types.Bool

Table of Contents

1 Prelude

2 Type of Booleans

The type of Booleans is inductively defined by two terms that we call "true" and "false".

data Bool : Type lzero where
  true : Bool
  false : Bool

{-# BUILTIN BOOL Bool #-}
{-# BUILTIN TRUE true #-}
{-# BUILTIN FALSE false #-}

We also define the "swap" function, which permutes the values of "true" and "false".

swap : Bool  Bool
swap true = false
swap false = true

Author: James Leslie

Created: 2021-03-27 Sat 10:47