------------------------------------------------------------------------
-- The Agda standard library
--
-- Byte Literals
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible #-}

module Data.Word8.Literals where

open import Agda.Builtin.FromNat using (Number)
open import Data.Unit.Base using (⊤)
open import Data.Word8.Base using (Word8; fromℕ)

number : Number Word8
number = record
  { Constraint = λ _ → ⊤
  ; fromNat    = λ w → fromℕ w
  }