]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/lambda-delta/syntax/sh.ma
confluence of parallel substitution (tps) started ...
[helm.git] / matita / matita / lib / lambda-delta / syntax / sh.ma
1 (*
2     ||M||  This file is part of HELM, an Hypertextual, Electronic
3     ||A||  Library of Mathematics, developed at the Computer Science
4     ||T||  Department of the University of Bologna, Italy.
5     ||I||
6     ||T||
7     ||A||  This file is distributed under the terms of the
8     \   /  GNU General Public License Version 2
9      \ /
10       V_______________________________________________________________ *)
11
12 include "lambda-delta/ground.ma".
13
14 (* SORT HIERARCHY ***********************************************************)
15
16 (* sort hierarchy specifications *)
17 record sh: Type[0] ≝ {
18    next: nat → nat;        (* next sort in the hierarchy *)
19    next_lt: ∀k. k < next k (* strict monotonicity condition *)
20 }.