kdrag.SeqStore

kdrag.SeqStore(s: SeqRef, i: ExprRef, v: ExprRef) → SeqRef

>>> _ = prove(SeqStore(seq(1,2,3), 2, 42) == seq(1,2,42))
>>> _ = prove(SeqStore(seq(1,2,3), 0, 42) == seq(42,2,3))

Parameters:

• s (SeqRef)

• i (ExprRef)

• v (ExprRef)

Return type:

SeqRef