kdrag.tele.has_type

kdrag.tele.has_type(ctx: Telescope, t0: ExprRef, T: SubSort, by=None, **kwargs) → Proof

Tactic to check that an expression t0 has type T in a context ctx.

>>> x = smt.Int("x")
>>> Nat = smt.Lambda([x], x >= 0)
>>> has_type([(x, Nat)], x+1, Nat)
|= Implies(And(x >= 0), Lambda(x, x >= 0)[x + 1])

Parameters:

• ctx (Telescope)

• t0 (ExprRef)

• T (SubSort)

Return type:

Proof