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



Index
This page has been generated by coqdoc