kdrag.tele.HasType

kdrag.tele.HasType(ctx: Telescope, t0: ExprRef, T: SubSort) → BoolRef

Formula that corresponds to typing judgement ctx |= t0 : T

>>> x = smt.Int("x")
>>> HasType([(x, Nat)], x+1, Pos)
Implies(And(x >= 0), Lambda(n, n > 0)[x + 1])

Parameters:

• ctx (Telescope)

• t0 (ExprRef)

• T (SubSort)

Return type:

BoolRef