]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/re_complete/basics/pts.ma
projects / helm.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
propagating the arithmetics library, partial commit
[helm.git] / matita / matita / re_complete / basics / pts.ma
1 include "basics/core_notation.ma".
2
3 universe constraint Type[0] < Type[1].
4 universe constraint Type[1] < Type[2].
5 universe constraint Type[2] < Type[3].
6 universe constraint Type[3] < Type[4].
7 universe constraint Type[4] < Type[5].
Unnamed repository; edit this file 'description' to name the repository.