From 32f2a8f8016b2c6c7fb88189fc0ea0c7f9336555 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 10 Sep 2009 15:12:05 +0000 Subject: [PATCH] ok, but slow on includes --- helm/software/matita/nlibrary/algebra/magmas.ma | 1 + helm/software/matita/nlibrary/sets/partitions.ma | 8 +++----- 2 files changed, 4 insertions(+), 5 deletions(-) diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma index 775cbd390..3e4cb942b 100644 --- a/helm/software/matita/nlibrary/algebra/magmas.ma +++ b/helm/software/matita/nlibrary/algebra/magmas.ma @@ -24,6 +24,7 @@ nrecord magma (A: magma_type) : Type[1] ≝ op_closed: ∀x,y. x ∈ mcarr → y ∈ mcarr → op A x y ∈ mcarr }. +alias symbol "hint_decl" = "hint_decl_Type2". unification hint 0 ≔ A : ? ⊢ carr1 (qpowerclass_setoid A) ≡ qpowerclass A. diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma index 3b17099a3..e83175f18 100644 --- a/helm/software/matita/nlibrary/sets/partitions.ma +++ b/helm/software/matita/nlibrary/sets/partitions.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "sets/sets.ma". -include "nat/plus.ma". +include "nat/plus.ma". (* tempi biblici neggli include che fa plus.ma *) include "nat/compare.ma". include "nat/minus.ma". include "datatypes/pairs.ma". @@ -26,6 +26,7 @@ alias symbol "eq" = "setoid1 eq". alias symbol "eq" = "setoid eq". alias symbol "eq" = "setoid1 eq". alias symbol "eq" = "setoid eq". +alias symbol "eq" = "setoid1 eq". nrecord partition (A: setoid) : Type[1] ≝ { support: setoid; indexes: qpowerclass support; @@ -114,10 +115,7 @@ ntheorem iso_nat_nat_union_pre: [##2: napply le_to_le_S_S; nassumption] napply ad_hoc15 [ nwhd in ⊢ (???(?%?)); - - napply (eq_rect_CProp0_r nat (n - i1) (λx.λy.?) ?? (minus_S_S …)); STOP - - nrewrite > (minus_S_S n i1); napply big_plus_preserves_ext; #i; #_; + napply big_plus_preserves_ext; #i; #_; nrewrite > (plus_n_S i i1); napply refl | nrewrite > (split_big_plus (S i1) i1 (λi.λ_.s i) ?) [##2: napply le_S; napply le_n] napply ad_hoc16; nrewrite > (minus_S i1); nnormalize; nrewrite > (plus_n_O (s i1) …); -- 2.39.2