-- The Agda primitives (preloaded).
{-# OPTIONS --cubical-compatible --no-import-sorts --level-universe #-}
module Agda.Primitive where
------------------------------------------------------------------------
-- Universe levels
------------------------------------------------------------------------
infixl 6 _⊔_
{-# BUILTIN PROP Prop #-}
{-# BUILTIN TYPE Set #-}
{-# BUILTIN STRICTSET SSet #-}
{-# BUILTIN PROPOMEGA Propω #-}
{-# BUILTIN SETOMEGA Setω #-}
{-# BUILTIN STRICTSETOMEGA SSetω #-}
{-# BUILTIN LEVELUNIV LevelUniv #-}
-- Level is the first thing we need to define.
-- The other postulates can only be checked if built-in Level is known.
postulate
Level : LevelUniv
-- MAlonzo compiles Level to (). This should be safe, because it is
-- not possible to pattern match on levels.
{-# BUILTIN LEVEL Level #-}
postulate
lzero : Level
lsuc : (ℓ : Level) → Level
_⊔_ : (ℓ₁ ℓ₂ : Level) → Level
{-# BUILTIN LEVELZERO lzero #-}
{-# BUILTIN LEVELSUC lsuc #-}
{-# BUILTIN LEVELMAX _⊔_ #-}
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