← Back

Modules

Leios

  • Abstract
  • Base
  • Blocks
  • Config
  • Defaults
  • FFD
  • Foreign.BaseTypes
  • Foreign.HsTypes
  • Foreign.Types
  • Foreign.Util
  • KeyRegistration
  • Network
  • Prelude
  • Protocol
  • Short
  • Short.Decidable
  • Short.Trace.Verifier
  • Short.Trace.Verifier.Test
  • Simplified
  • Simplified.Deterministic
  • SpecStructure
  • Traces
  • Voting
  • VRF

Network

  • BasicBroadcast
  • Leios
123456789101112131415
{-# OPTIONS --cubical-compatible --safe --no-universe-polymorphism
--no-sized-types --no-guardedness --level-universe #-}
 
module Agda.Builtin.Bool where
 
data Bool : Set where
false true : Bool
 
{-# BUILTIN BOOL Bool #-}
{-# BUILTIN FALSE false #-}
{-# BUILTIN TRUE true #-}
 
{-# COMPILE JS Bool = function (x,v) { return ((x)? v["true"]() : v["false"]()); } #-}
{-# COMPILE JS false = false #-}
{-# COMPILE JS true = true #-}