]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/lambda-delta/syntax/lenv.ma
confluence of parallel substitution (tps) started ...
[helm.git] / matita / matita / lib / lambda-delta / syntax / lenv.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/syntax/term.ma".
13
14 (* LOCAL ENVIRONMENTS *******************************************************)
15
16 (* local environments *)
17 inductive lenv: Type[0] ≝
18 | LSort: lenv                       (* empty *)
19 | LPair: lenv → bind2 → term → lenv (* binary binding construction *)
20 .
21
22 interpretation "sort (local environment)" 'Star = LSort.
23
24 interpretation "environment binding construction (binary)" 'DBind L I T = (LPair L I T).