{-# OPTIONS --without-K #-}

module Agda.Builtin.Size where

{-# BUILTIN SIZEUNIV SizeU #-}
{-# BUILTIN SIZE     Size   #-}
{-# BUILTIN SIZELT   Size<_ #-}
{-# BUILTIN SIZESUC  ↑_     #-}
{-# BUILTIN SIZEINF  ω      #-}
{-# BUILTIN SIZEMAX  _⊔ˢ_  #-}