Syntax Definition ht 2

Description: The type of all functions from type α to type β.

Hypotheses

Ref	Expression
hal	type α
hbe	type β

Assertion

Ref	Expression
ht	type (α → β)

See definition weq 38 for more information.