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