src/Logic/Theory/Semigroup.hs

   1 {-# LANGUAGE Safe #-}
   2 {-# OPTIONS_GHC -Wno-unused-top-binds #-}
   3
   4 module Logic.Theory.Semigroup (
   5   type (<>) (),
   6   (<>),
   7   type NonEmptyConcat (),
   8   sconcat,
   9 ) where
  10
  11 import Data.List.NonEmpty qualified as NonEmpty
  12 import Data.Semigroup qualified as Semigroup
  13 import Logic.Kernel
  14 import Logic.Theory.Arithmetic
  15 import Logic.Theory.List
  16 import Logic.Theory.Ord
  17
  18 data (<>) aN bN = AppendAxiom
  19 type role (<>) nominal nominal
  20
  21 data NonEmptyConcat aN = NonEmptyConcatAxiom
  22 type role NonEmptyConcat nominal
  23
  24 (<>) :: Semigroup.Semigroup a => aN ::: a -> bN ::: a -> (<>) aN bN ::: a
  25 (<>) (Named x) (Named y) = AppendAxiom ... (x Semigroup.<> y)
  26
  27 sconcat :: Semigroup.Semigroup a => aN ::: [a] / Zero < ListLength aN -> NonEmptyConcat aN ::: a
  28 sconcat (Named xs) = NonEmptyConcatAxiom ... Semigroup.sconcat (NonEmpty.fromList xs)