X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fsequence.ma;h=948d14f67963ef2e929bba924e40edbe58572ea4;hb=6b61a9e6698a7c1936adf217b599e34e65a5e4c9;hp=44620ba39e2f5377ca8e068e40ee2d4e14612277;hpb=d4302f43737034a69bd475e5f46e8d126229375e;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/sequence.ma b/helm/software/matita/contribs/dama/dama/sequence.ma
index 44620ba39..948d14f67 100644
--- a/helm/software/matita/contribs/dama/dama/sequence.ma
+++ b/helm/software/matita/contribs/dama/dama/sequence.ma
@@ -12,10 +12,27 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "excess.ma".
+include "nat/nat.ma".
 
-definition sequence := λO:Type.nat → O.
+inductive sequence (O:Type) : Type ≝  
+ | mk_seq : (nat → O) → sequence O.
 
-definition fun_of_sequence: ∀O:Type.sequence O → nat → O ≝ λO.λx:sequence O.x.
+definition fun_of_seq: ∀O:Type.sequence O → nat → O ≝ 
+  λO.λx:sequence O.match x with [ mk_seq f ⇒ f ].
 
-coercion cic:/matita/sequence/fun_of_sequence.con 1.
+coercion cic:/matita/dama/sequence/fun_of_seq.con 1.
+
+notation < "hvbox((\lfloor term 19 p \rfloor) \sub ident i)" with precedence 90
+for @{ 'sequence (\lambda ${ident i} : $t . $p)}.
+
+notation > "hvbox((\lfloor term 19 p \rfloor) \sub ident i)" with precedence 90
+for @{ 'sequence (\lambda ${ident i} . $p)}.
+
+notation > "hvbox(\lfloor ident i, term 19 p \rfloor)" with precedence 90
+for @{ 'sequence (\lambda ${ident i} . $p)}.
+  
+notation "a \sub i" left associative with precedence 90 
+  for @{ 'sequence_appl $a $i }.
+
+interpretation "sequence" 'sequence \eta.x = (mk_seq _ x).
+interpretation "sequence element" 'sequence_appl s i = (fun_of_seq _ s i).