kdrag.theories.seq.Head

kdrag.theories.seq.Head(s: SeqRef)

>>> x = smt.Const("x", Seq(smt.BoolSort()))
>>> Head(x)
Nth(x, 0)
>>> kd.prove(smt.Implies(smt.Length(x) > 0, smt.Concat([smt.Unit(Head(x)), Tail(x)]) == x))
|= Implies(Length(x) > 0,
    Concat(Unit(Nth(x, 0)),
            seq.extract(x, 1, Length(x) - 1)) ==
    x)

Parameters:

s (SeqRef)