From 9b3a308c7248fd2fa94162e4401726327cc66aa3 Mon Sep 17 00:00:00 2001 From: Peter Mikkelsen Date: Wed, 23 Jun 2021 16:20:51 +0000 Subject: Add some agda test --- .../_tmp/agda-dfa/Agda.Primitive.html | 35 ++++++++++++++++++++++ 1 file changed, 35 insertions(+) create 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 new file mode 100644 index 0000000..5829754 --- /dev/null +++ b/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.html @@ -0,0 +1,35 @@ + +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