From The Twelf Project
Jump to: navigation, search

It is common to refer to a an LF type family as a relation, because a type family defines a relation on its indices where indices are related iff their instance of the type family is inhabited. A htype family is also commonly referred to as a judgment.

See also

This page is incomplete. We should expand it.