X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Flists%2Flist.ma;h=c89bb78560b5ac1b1a9dbb061a372e85318afd9a;hb=f0d422b660e11886ec4f9a823da795050f07e07f;hp=ff7fcf80f8ee973cbec708aefa8c076365826018;hpb=eaaea3c18083de3e442e939768ff450d3b093911;p=helm.git

diff --git a/matita/matita/lib/basics/lists/list.ma b/matita/matita/lib/basics/lists/list.ma
index ff7fcf80f..c89bb7856 100644
--- a/matita/matita/lib/basics/lists/list.ma
+++ b/matita/matita/lib/basics/lists/list.ma
@@ -55,6 +55,11 @@ definition hd ≝ λA.λl: list A.λd:A.
 
 definition tail ≝  λA.λl: list A.
   match l with [ nil ⇒  [] | cons hd tl ⇒  tl].
+  
+definition option_hd ≝ 
+  λA.λl:list A. match l with
+  [ nil ⇒ None ?
+  | cons a _ ⇒ Some ? a ].
 
 interpretation "append" 'append l1 l2 = (append ? l1 l2).