blob: 58ef1b7ce81f3ec053127aa910969c4eb2b8150a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
Additive : Type -> Type
Additive A = { zero : A; plus : A -> A -> A }
additive_Integer : Additive Integer
additive_Integer = { zero = 0; plus = prim_add_Int }
sum : (A:Type) -> Additive A -> List A -> A
sum _ d (Nil _) = d.zero
sum A d (Cons _ x xs) = d.plus x (sum A d xs)
Showable : Type -> Type
Showable A = { show : A -> String }
--Compositional : Type -> Type
--Compositional A = { composOp : }
|
