kdrag.theories.real.vec

Functions

Fin0Sort(N)	A different style of finsort
FinSort(N)	Make a finite enumeration.
FunVec(N)
SeqVec(N)
Vec(N)
Vec0(N)

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

A different style of finsort

>>> Fin0Sort(3)
Option_Option_Unit

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

Make a finite enumeration.

>>> FinSort(3)
Fin3

kdrag.theories.real.vec.FunVec(N: ExprRef | int)

Parameters:

N (ExprRef | int)

kdrag.theories.real.vec.SeqVec(N: ExprRef | int)

Parameters:

N (ExprRef | int)

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)
Vec0_2.dot(u, v)

Parameters:

N (int)

Return type:

DatatypeSortRef