/usr/share/agda-stdlib/Size.agda is in agda-stdlib 0.6-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 | ------------------------------------------------------------------------
-- The Agda standard library
--
-- Sizes for Agda's sized types
------------------------------------------------------------------------
module Size where
postulate
Size : Set
↑_ : Size → Size
∞ : Size
{-# BUILTIN SIZE Size #-}
{-# BUILTIN SIZESUC ↑_ #-}
{-# BUILTIN SIZEINF ∞ #-}
|