kdrag.theories.real.vec.Vec0

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)