(* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************)
definition nta (a) (h): relation4 genv lenv term term ≝
(* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************)
definition nta (a) (h): relation4 genv lenv term term ≝
- λG,L,T,U. ⦃G,L⦄ ⊢ ⓝU.T ![a,h].
+ λG,L,T,U. ⦃G,L⦄ ⊢ ⓝU.T ![a,h].
interpretation "native type assignment (term)"
'Colon a h G L T U = (nta a h G L T U).
interpretation "restricted native type assignment (term)"
interpretation "native type assignment (term)"
'Colon a h G L T U = (nta a h G L T U).
interpretation "restricted native type assignment (term)"