X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Ftopology%2Figft.ma;h=d35030b3553932a3f033b5c811f8911503c7c2e6;hb=32af98424d4320a4a38fff23ac0398e026fe0ffc;hp=ce02f95df55f5327341d25fa8fc4d4ffcac88bb3;hpb=f1c4852a4359cf278ed00d73d608856ff46bafbb;p=helm.git

diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index ce02f95df..d35030b35 100644
--- a/helm/software/matita/nlibrary/topology/igft.ma
+++ b/helm/software/matita/nlibrary/topology/igft.ma
@@ -823,27 +823,25 @@ Appendix: natural deduction like tactics explanation
 -----------------------------------------------------
 
 In this appendix we try to give a description of tactics
-in terms of natural deduction rules annotated with proofs.
+in terms of sequent calculus rules annotated with proofs.
 The `:` separator has to be read as _is a proof of_, in the spirit
 of the Curry-Howard isomorphism.
 
-                  f  :  A1 → … → An → B    ?1 : A1 … ?n  :  An 
-    napply f;    ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
-                           (f ?1 … ?n )  :  B
+                  Γ ⊢  f  :  A1 → … → An → B    Γ ⊢ ?1 : A1 … ?n  :  An 
+    napply f;    ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
+                           Γ ⊢ (f ?1 … ?n )  :  B
  
 foo  
 
-                               [x : T]
-                                  ⋮  
-                               ?  :  P(x) 
+                         Γ; x : T  ⊢ ?  :  P(x) 
     #x;         ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
-                            λx:T.?  :  ∀x:T.P(x)
+                         Γ ⊢ λx:T.?  :  ∀x:T.P(x)
 
 baz
                        
-                 (?1 args1)  :  P(k1 args1)  …  (?n argsn)  :  P(kn argsn)         
-    ncases x;   ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
-                   match x with k1 args1 ⇒ ?1 | … | kn argsn ⇒ ?n  :  P(x)                    
+                 Γ; args… : Args… ⊢ ?i  :  P(k1 args1)  …  (?n argsn)  :  P(kn argsn)         
+    ncases x;   ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼
+                 Γ ⊢ match x with k1 args1 ⇒ ?1 | … | kn argsn ⇒ ?n  :  P(x)                    
 
 bar