(****************************************************************************) (* *) (* The formal system \lambda\delta *) (* *) (* Author: Ferruccio Guidi *) (* *) (* This file is distributed under the terms of the *) (* GNU General Public License Version 2 *) (* *) (****************************************************************************) Require Export parameter_defs. Require Export pc3_defs. Inductive ty3 [g:G]: C -> T -> T -> Prop := | ty3_conv: (c:?; t2,t:?) (ty3 g c t2 t) -> (u,t1:?) (ty3 g c u t1) -> (pc3 c t1 t2) -> (ty3 g c u t2) | ty3_sort: (c:?; m:?) (ty3 g c (TSort m) (TSort (next g m))) | ty3_abbr: (n:?; c,d:?; u:?) (getl n c (CHead d (Bind Abbr) u)) -> (t:?) (ty3 g d u t) -> (ty3 g c (TLRef n) (lift (S n) (0) t)) | ty3_abst: (n:?; c,d:?; u:?) (getl n c (CHead d (Bind Abst) u)) -> (t:?) (ty3 g d u t) -> (ty3 g c (TLRef n) (lift (S n) (0) u)) | ty3_bind: (c:?; u,t:?) (ty3 g c u t) -> (b:?; t1,t2:?) (ty3 g (CHead c (Bind b) u) t1 t2) -> (ty3 g c (THead (Bind b) u t1) (THead (Bind b) u t2)) | ty3_appl: (c:?; w,u:?) (ty3 g c w u) -> (v,t:?) (ty3 g c v (THead (Bind Abst) u t)) -> (ty3 g c (THead (Flat Appl) w v) (THead (Flat Appl) w (THead (Bind Abst) u t)) ) | ty3_cast: (c:?; t1,t2:?) (ty3 g c t1 t2) -> (t0:?) (ty3 g c t2 t0) -> (ty3 g c (THead (Flat Cast) t2 t1) (THead (Flat Cast) t0 t2)). Hints Resolve ty3_sort ty3_abbr ty3_abst ty3_bind ty3_appl ty3_cast : ld. Inductive tys3 [g:G; c:C]: TList -> T -> Prop := | tys3_nil: (u,u0:?) (ty3 g c u u0) -> (tys3 g c TNil u) | tys3_cons: (t,u:?) (ty3 g c t u) -> (ts:?) (tys3 g c ts u) -> (tys3 g c (TCons t ts) u). Hint tys3 : ld := Constructors tys3.