partial commit in static_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / syntax / sh.ma

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/sh.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/sh.ma
index 8129473752d35bd95146f95897f66fe65431a75f..9e9b8adc173d9d572be15726499bf99b27b4c0d0 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/sh.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/sh.ma
@@ -12,18 +12,18 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/lib/arith.ma".
-include "static_2/notation/functions/upspoon_2.ma".
+include "ground/arith/nat.ma".
+include "static_2/notation/functions/uparrow_1_0.ma".
 
 (* SORT HIERARCHY ***********************************************************)
 
 (* sort hierarchy specification *)
 record sh: Type[0] ≝ {
-  next: nat → nat (* next sort in the hierarchy *)
+  sh_next: nat → nat (* next sort in the hierarchy *)
 }.
 
 interpretation "next sort (sort hierarchy)"
-   'UpSpoon h s = (next h s).
+   'UpArrow_1_0 h = (sh_next h).
 
 definition sh_is_next (h): relation nat ≝
-           λs1,s2. ⫯[h]s1 = s2.
+           λs1,s2. â\87¡[h]s1 = s2.