Denotational Semantics in Agda
Data.Bool
Initializing search
    pdmosses/xds-agda
    • About
    • Meta-notation
    • ULC
    • PCF
    • Scheme
    pdmosses/xds-agda
    • About
    • Meta-notation
      • Untyped λ-calculus
      • ULC.All
      • ULC.Variables
      • ULC.Terms
      • ULC.Domains
      • ULC.Environments
      • ULC.Semantics
      • ULC.Checks
      • PCF (Plotkin 1977)
      • PCF.All
      • PCF.Domain Notation
      • PCF.Types
      • PCF.Constants
      • PCF.Variables
      • PCF.Terms
      • PCF.Environments
      • PCF.Checks
      • Core Scheme (R5RS)
      • Scheme.All
      • Scheme.Domain Notation
      • Scheme.Abstract Syntax
      • Scheme.Domain Equations
      • Scheme.Auxiliary Functions
      • Scheme.Semantic Functions

    Data.Bool

    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Booleans
    ------------------------------------------------------------------------
    
    {-# OPTIONS --cubical-compatible --safe #-}
    
    module Data.Bool where
    
    ------------------------------------------------------------------------
    -- The boolean type and some operations
    
    open import Data.Bool.Base public
    
    ------------------------------------------------------------------------
    -- Publicly re-export queries
    
    open import Data.Bool.Properties public
      using (T?; _≟_; _≤?_; _<?_)
    
    Made with Material for MkDocs