kdrag.tele.Id

kdrag.tele.Id(x: ExprRef, y: ExprRef) → SubSort

>>> x, y = smt.Ints("x y")
>>> p = smt.Const("p", Unit)
>>> has_type([x], Unit.tt, Id(x, x))
|= Implies(And(True), Lambda(p!..., x == x)[tt])
>>> has_type([x, y, (p, Id(x,y))], Unit.tt, Id(y, x))
|= Implies(And(True, True, x == y), Lambda(p!..., y == x)[tt])

Parameters:

• x (ExprRef)

• y (ExprRef)

Return type:

SubSort