Skip to main content

Questions tagged [type-rule]

In type theory, a type rule is an inference rule that describes how a type system assigns a type to a syntactic construction. These rules may be applied by the type system to determine if a program is well typed and what type expressions have. (from Wikipedia)

Filter by
Sorted by
Tagged with
18 votes
2 answers
599 views

What is the difference between judgmental equality, definitional equality, and equality types?

This answer to this question about η-equivalence in Coq draws a distinction between judgmental equality and definitional equality. In the simply typed lambda calculus (henceforth STLC), the following ...
Greg Nisbet's user avatar
  • 2,771