Type family

From The Twelf Project
Jump to: navigation, search

We use the word type family to refer to the syntactic class of LF that classifies terms and is classified by kinds. The type families include the types of LF, which are dependent function types and type family constants that are fully applied to arguments. The type families also include partially applied type family constants. We refer to the arguments of a type family constant as the subjects or indices of the family.

The LF methodology specifies how object-language judgements are represented as LF type families.

See also

This page is incomplete. We should expand it.