calculus/Calculus/Lambda/Omega/Explicit/lib/Monoid.cloe

   1 Monoid_Mempty  (M:*) = M
   2 Monoid_Mappend (M:*) = M -> M -> M
   3
   4 Monoid_Class
   5  (M:*) (Data:*)
   6  =  (mempty:Monoid_Mempty M)
   7  -> (mappend:Monoid_Mappend M)
   8  -> Data
   9 Monoid_Polytype
  10  (M:*) : *p
  11  = (Data:*) -> Monoid_Class M Data -> Data
  12 Monoid
  13  (M:*) : *m
  14  = Monotype (Monoid_Polytype M)
  15
  16 monoid
  17  (M:*)
  18  (mempty:Monoid_Mempty M)
  19  (mappend:Monoid_Mappend M)
  20  : Monoid M
  21  = monotype (Monoid_Polytype M)
  22     (λ(Data:*) (monoid_class:Monoid_Class M Data) ->
  23       monoid_class mempty mappend)
  24 unMonoid
  25  (M:*) (Data:*)
  26  (monoid_class:Monoid_Class M Data)
  27  (monoid:Monoid M)
  28  : Data
  29  = polytype (Monoid_Polytype M) monoid Data monoid_class
  30
  31 Monoid_mempty
  32  (M:*) (monoid:Monoid M)
  33  : Monoid_Mempty M
  34  = unMonoid M (Monoid_Mempty M)
  35     (λ(mempty:Monoid_Mempty M) (mappend:Monoid_Mappend M) -> mempty)
  36     monoid
  37 Monoid_mappend
  38  (M:*) (monoid:Monoid M)
  39  : Monoid_Mappend M
  40  = unMonoid M (Monoid_Mappend M)
  41     (λ(mempty:Monoid_Mempty M) (mappend:Monoid_Mappend M) -> mappend)
  42     monoid