kdrag.theories.algebra.group

Classes

`AbelSemiGroup`(*L)
`Group`(*L)
`Monoid`(*L)
`Semigroup`(*L)

class kdrag.theories.algebra.group.AbelSemiGroup(*L)

Bases: TypeClass

assert_eq(a, b)

check(T)

comm: Proof

classmethod get_registry() → dict

Return type:: dict

key: SortRef

classmethod lookup(*L)

classmethod register(*L, **kwargs)

class kdrag.theories.algebra.group.Group(*L)

Bases: TypeClass

assert_eq(a, b)

check(T)

classmethod get_registry() → dict

Return type:: dict

inv: FuncDeclRef

inv_left: Proof

inv_right: Proof

classmethod lookup(*L)

classmethod register(*L, **kwargs)

class kdrag.theories.algebra.group.Monoid(*L)

Bases: TypeClass

assert_eq(a, b)

check(T)

e: ExprRef

classmethod get_registry() → dict

Return type:: dict

id_left: Proof

id_right: Proof

classmethod lookup(*L)

classmethod register(*L, **kwargs)

class kdrag.theories.algebra.group.Semigroup(*L)

Bases: TypeClass

assert_eq(a, b)

assoc: Proof

check(T)

classmethod get_registry() → dict

Return type:: dict

key: SortRef

classmethod lookup(*L)

classmethod register(*L, **kwargs)