AST to ASTFE completed up to a few computational (!!!) axioms.

[helm.git] / helm / software / matita / contribs / assembly / compiler / utility.ma

diff --git a/helm/software/matita/contribs/assembly/compiler/utility.ma b/helm/software/matita/contribs/assembly/compiler/utility.ma
index 4352dc426ce24939cf091534d25c48979e514d83..aef219e06b90d17994ca6a0f9e916100121e31af 100755 (executable)
--- a/helm/software/matita/contribs/assembly/compiler/utility.ma
+++ b/helm/software/matita/contribs/assembly/compiler/utility.ma
@@ -40,7 +40,7 @@ notation "hvbox(hd break §§ tl)"
   right associative with precedence 46
   for @{'ne_cons $hd $tl}.
 
-notation "« y £ break list0 x sep ; »"
+notation "« y break £ list0 x sep ; break »"
   non associative with precedence 90
   for ${fold right @{'ne_nil $y } rec acc @{'ne_cons $x $acc}}.
 
@@ -134,6 +134,28 @@ definition cut_last_neList ≝
  [ ne_nil h ⇒ ne_nil T h
  | ne_cons _ t ⇒ reverse_neList T t ].
 
+(* getFirst *)
+definition get_first_list ≝
+λT:Type.λl:list T.match l with
+ [ nil ⇒ None ?
+ | cons h _ ⇒ Some ? h ].
+
+definition get_first_neList ≝
+λT:Type.λl:ne_list T.match l with
+ [ ne_nil h ⇒ h
+ | ne_cons h _ ⇒ h ].
+
+(* cutFirst *)
+definition cut_first_list ≝
+λT:Type.λl:list T.match l with
+ [ nil ⇒ nil T
+ | cons _ t ⇒ t ].
+
+definition cut_first_neList ≝
+λT:Type.λl:ne_list T.match l with
+ [ ne_nil h ⇒ ne_nil T h
+ | ne_cons _ t ⇒ t ].
+
 (* apply f *)
 let rec apply_f_list (T1,T2:Type) (l:list T1) (f:T1 → T2) on l ≝
 match l with