Semiring import boilerplate

agda · Sep 10, 2023 · 0d2a853 · 0d2a853
1 parent 4894009
commit 0d2a853
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/Cubical/Algebra/Semiring.agda b/Cubical/Algebra/Semiring.agda
@@ -0,0 +1,4 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.Semiring where
+
+open import Cubical.Algebra.Semiring.Base public