ulkb.Expression.instantiate

Expression.instantiate(theta)

Applies type-variable instantiation theta to expression.

Parameters:

theta – Dictionary mapping type variables to types.

Returns:

The resulting Expression.

Example:

a, b = TypeVariables('a', 'b')
f = Constant('f', FunctionType(a, b))
x = Variable('x', a)

print(f(x))
# (f : a → b) (x : a)

print(f(x).instantiate({a: BaseType('nat'), b: BoolType()}))
# (f : nat → bool) (x : nat)