------------------------------------------------------------------------
-- The Agda standard library
--
-- Sizes for Agda's sized types
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --sized-types #-}
module Size where
open import Level
------------------------------------------------------------------------
-- Re-export builtins
open import Agda.Builtin.Size public using
( SizeUniv -- sort SizeUniv
; Size -- : SizeUniv
; Size<_ -- : Size → SizeUniv
; ↑_ -- : Size → Size
; _⊔ˢ_ -- : Size → Size → Size
; ∞ -- : Size
)
------------------------------------------------------------------------
-- Concept of sized type
SizedSet : (ℓ : Level) → Set (suc ℓ)
SizedSet ℓ = Size → Set ℓ
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4