kdrag.theories.real.vec

Functions

FinSort(N)	Make a finite enumeration.
Vec(N)
Vec0(N)

kdrag.theories.real.vec.FinSort(N)

Make a finite enumeration.

>>> FinSort(3)
Fin3

kdrag.theories.real.vec.Vec(N)

kdrag.theories.real.vec.Vec0(N: int) → DatatypeSortRef

>>> Vec2 = Vec0(2)
>>> u, v = smt.Consts("u v", Vec2)
>>> u[1]
val(u)[X1]
>>> dot(u, v)
dot(u, v)

Parameters:

N (int)

Return type:

DatatypeSortRef