include "ground/arith/pnat.ma".
include "delayed_updating/notation/functions/nodelabel_d_1.ma".
+include "delayed_updating/notation/functions/nodelabel_m_0.ma".
include "delayed_updating/notation/functions/edgelabel_l_0.ma".
include "delayed_updating/notation/functions/edgelabel_a_0.ma".
include "delayed_updating/notation/functions/edgelabel_s_0.ma".
(* LABEL ********************************************************************)
inductive label: Type[0] ≝
-| label_node_d: pnat → label
-| label_edge_l: label
-| label_edge_a: label
-| label_edge_s: label
+| label_d: pnat → label
+| label_m: label
+| label_L: label
+| label_A: label
+| label_S: label
.
-coercion label_node_d.
-
interpretation
"variable reference by depth (label)"
- 'NodeLabelD p = (label_node_d p).
+ 'NodeLabelD p = (label_d p).
+
+interpretation
+ "mark (label)"
+ 'NodeLabelM = (label_m).
interpretation
"name-free functional abstruction (label)"
- 'EdgeLabelL = (label_edge_l).
+ 'EdgeLabelL = (label_L).
interpretation
"application (label)"
- 'EdgeLabelA = (label_edge_a).
+ 'EdgeLabelA = (label_A).
interpretation
"side branch (label)"
- 'EdgeLabelS = (label_edge_s).
+ 'EdgeLabelS = (label_S).