From 9cb56dabb676391a9382731347e8d2b07b9437a5 Mon Sep 17 00:00:00 2001 From: Peter Mikkelsen Date: Sun, 7 Apr 2024 13:25:49 +0200 Subject: big cleanup --- .../_tmp/agda-dfa/Agda.Primitive.html | 35 ---------------------- 1 file changed, 35 deletions(-) delete mode 100644 sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.html (limited to 'sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.html') diff --git a/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.html b/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.html deleted file mode 100644 index 5829754..0000000 --- a/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.html +++ /dev/null @@ -1,35 +0,0 @@ - -Agda.Primitive
-- The Agda primitives (preloaded).
-
-{-# OPTIONS --without-K --no-subtyping #-}
-
-module Agda.Primitive where
-
-------------------------------------------------------------------------
--- Universe levels
-------------------------------------------------------------------------
-
-infixl 6 _⊔_
-
--- Level is the first thing we need to define.
--- The other postulates can only be checked if built-in Level is known.
-
-postulate
-  Level : Set
-
--- 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  _⊔_   #-}
-
-{-# BUILTIN SETOMEGA Setω #-}
-
\ No newline at end of file -- cgit v1.2.3