mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-10-26 08:09:22 +03:00
Added Sumbonoid
This commit is contained in:
parent
b1f3b4e77d
commit
e2e83e6c07
3
base/Monoid/get_e.kind
Normal file
3
base/Monoid/get_e.kind
Normal file
@ -0,0 +1,3 @@
|
||||
Monoid.get_e<A: Type>(M: Monoid(A)): A
|
||||
open M
|
||||
M.e
|
4
base/Monoid/get_op.kind
Normal file
4
base/Monoid/get_op.kind
Normal file
@ -0,0 +1,4 @@
|
||||
// Returns the monoid operation for the given monoid.
|
||||
Monoid.get_op<A: Type>(M: Monoid<A>): A -> A -> A
|
||||
open M
|
||||
M.op
|
7
base/Submonoid.kind
Normal file
7
base/Submonoid.kind
Normal file
@ -0,0 +1,7 @@
|
||||
type Submonoid<A: Type>(M: Monoid(A)){
|
||||
new(
|
||||
Q: A -> Type,
|
||||
he: Q(Monoid.get_e(A,M)),
|
||||
closed: (a: A) (ha: Q(a)) (b: A) (hb: Q(b)) -> Q(Monoid.get_op(A,M)(a, b)),
|
||||
)
|
||||
}
|
Loading…
Reference in New Issue
Block a user