From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 4 Mar 2014 21:52:05 +0000 (+0000)
Subject: a suggestion was added to avoid 1 pseudo reduction at the cost of 40 proper
X-Git-Tag: make_still_working~958
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=672cb6cc509b233d3201ea4b5959b65980323bf7;p=helm.git

a suggestion was added to avoid 1 pseudo reduction at the cost of 40 proper
reductions :(
---

diff --git a/helm/software/helena/examples/grundlagen/grundlagen.aut b/helm/software/helena/examples/grundlagen/grundlagen.aut
index 4a856c245..d38532d36 100644
--- a/helm/software/helena/examples/grundlagen/grundlagen.aut
+++ b/helm/software/helena/examples/grundlagen/grundlagen.aut
@@ -2,6 +2,7 @@
 # Copyright (C) 1977, L.S. van Benthem Jutting
 #               1992, revised by F. Wiedijk (http://www.cs.ru.nl/~freek/aut/)
 #               2008, revised by F. Guidi to remove the eta-reductions
+#               2014, revised by F. Guidi to suggest @-typing removal
 
 +l
 @[a:'prop'][b:'prop']
@@ -681,8 +682,12 @@ th2:=[x:a]cone(<x>b,mp"l"(a,con,x,n)):imp(a,b)
 b@ec:=[x:a]not(<x>b):'prop'
 [n:not(a)]
 eci1:=[x:a]cone(not(<x>b),mp"l"(a,con,x,n)):ec(a,b)
-b@[a1:and(a,b)]
-ande2:=<ande1(a,b,a1)>ande2"l"(a,b,a1):<ande1(a,b,a1)>b
+%suggestion by Guidi to remove @-typing
+b@[a1:and(a,b)] %original line
+ande2:=<ande1(a,b,a1)>ande2"l"(a,b,a1):<ande1(a,b,a1)>b %original line
+%b@[a1:and(a,[x:a]<x>b)]
+%ande2:=<ande1(a,[x:a]<x>b,a1)>ande2"l"(a,[x:a]<x>b,a1):<ande1(a,[x:a]<x>b,a1)>[x:a]<x>b
+%end of suggestion
 a@[ksi:'type']
 +ite
 [x1:ksi][y1:ksi]