From: Enrico Tassi Date: Mon, 9 Jul 2007 13:32:17 +0000 (+0000) Subject: added few more fun to this test X-Git-Tag: make_still_working~6209 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f797f67a51e6c9919d77429cf0b9d7a747554eb0;p=helm.git added few more fun to this test --- diff --git a/helm/software/matita/tests/multiple_inheritance.ma b/helm/software/matita/tests/multiple_inheritance.ma index 413c42d44..df15e704f 100644 --- a/helm/software/matita/tests/multiple_inheritance.ma +++ b/helm/software/matita/tests/multiple_inheritance.ma @@ -28,19 +28,20 @@ record R : Type := { r1 :> R1; r2_ : R2; with_: C r1 = K r2_ }. lemma r2 : R → R2. intro; apply mk_R2; - [ apply (C r) - | apply (eq_rect ? ? (λx.x → x → x)); - [3: symmetry; - [2: apply (with_ r) - | skip - ] - | skip - | apply (mult (r2_ r)) - ] - ]. + [ exact (C r) + | rewrite > (with_ r); exact (mult (r2_ r))] qed. coercion cic:/matita/test/r2.con. +(* convertibility test *) +lemma conv_test : ∀r:R.C r -> K r. + intros. + change with (C (r1 r)). + change with (K (r2 r)). + change with (C (r1 r)). + assumption. +qed. + (* Let's play with it *) definition f ≝ λr:R.λx:r.plus ? (mult ? x x) x. @@ -51,4 +52,7 @@ lemma test: ∀r:R. ∀x:r. f ? x = x. intros; unfold f; autobatch paramodulation. -qed. \ No newline at end of file +qed. + + +