Library base

Abstract Parameters of PTS

A PTS depends on two sets that control typing of sorts and Π-types, and two other sets that define what is a sort and what is a variable.

Sorts and Variables

Sorts can be anything we want:
Module Type term_sig.
Interactive Module Type term_sig started

  Parameter Sorts : Set.
Sorts is assumed

End term_sig.
Module Type term_sig is defined

Module Type pts_sig (X:term_sig).
Interactive Module Type pts_sig started

  Import X.

Ax is used to type Sorts.
  Parameter Ax : Sorts -> Sorts -> Prop.
Ax is assumed

Rel is used to type Π-types.
  Parameter Rel : Sorts -> Sorts -> Sorts -> Prop.
Rel is assumed

End pts_sig.
Module Type pts_sig is defined

To deal with variable binding, we use de Bruijn indexes:
Definition Vars := nat.
Vars is defined

This page has been generated by coqdoc