Prim.Data.Bool

1Lab
  • Primitive: Booleans🔗


back to index
view all pages
link to source

Written by Amélia Liao

back to index
open import Prim.Extension
open import Prim.Interval
open import Prim.Type
open import Prim.Kan

module Prim.Data.Bool where

Primitive: Booleans🔗

The booleans are the h-initial type with two inhabitants.

data Bool : Type where
  true false : Bool
{-# BUILTIN BOOL Bool #-}

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