kdrag.theories.algebra.vector

Module Attributes

zero_add

V.smul = smt.Function("smul", V, smt.RealSort(), V) kd.notation.mul.register(V, smul) x, y = smt.Reals("x y")

Classes

Normed(*L)	https://en.wikipedia.org/wiki/Normed_vector_space
VectorSpace(*L)

class kdrag.theories.algebra.vector.Normed(*L)

Bases: TypeClass

https://en.wikipedia.org/wiki/Normed_vector_space

assert_eq(a, b)

check(T)

classmethod get_registry() → dict

Return type:

dict

key: SortRef

classmethod lookup(*L)

norm: FuncDeclRef

norm_homog: Proof

norm_nonneg: Proof

norm_triangle: Proof

norm_zero: Proof

classmethod register(*L, **kwargs)

class kdrag.theories.algebra.vector.VectorSpace(*L)

Bases: TypeClass

add_assoc: Proof

add_comm: Proof

add_inv: Proof

add_zero: Proof

assert_eq(a, b)

check(T)

classmethod get_registry() → dict

Return type:

dict

key: SortRef

classmethod lookup(*L)

classmethod register(*L, **kwargs)

scalar: SortRef

smul: FuncDeclRef

smul_assoc: Proof

smul_distrib: Proof

zero: ExprRef

kdrag.theories.algebra.vector.zero_add = |= ForAll(u, vadd(zero, u) == u)

V.smul = smt.Function(“smul”, V, smt.RealSort(), V) kd.notation.mul.register(V, smul) x, y = smt.Reals(“x y”)

smul_one = kd.axiom(smt.ForAll([u], u * 1 == u))

# Possible design for theories. vadd = kd.notation.SortDispatch() vadd_assoc = {V: add_assoc} vadd_comm = {V: add_comm}

vzero = {V: zero} vadd_zero = {V: add_zero}

Parameters:

args (smt.ExprRef | Proof)