From 496f18d45b7fef262fd3fe42bab0d617a866bcf9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 7 Jan 2011 14:00:29 +0000 Subject: [PATCH] non uniform coercion names in sync with the TYPES talk, stil commented out... --- matita/matita/lib/hints_declaration.ma | 28 +++++++++++++------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/matita/matita/lib/hints_declaration.ma b/matita/matita/lib/hints_declaration.ma index bcbfed4f3..d04f453f2 100644 --- a/matita/matita/lib/hints_declaration.ma +++ b/matita/matita/lib/hints_declaration.ma @@ -72,22 +72,23 @@ interpretation "hint_decl_CProp1" 'hint_decl a b = (hint_declaration_CProp1 ? a interpretation "hint_decl_CProp0" 'hint_decl a b = (hint_declaration_CProp0 ? a b). interpretation "hint_decl_Type0" 'hint_decl a b = (hint_declaration_Type0 ? a b). -(* Non uniform coercions support -record lock2 (S : Type[2]) (s : S) : Type[3] ≝ { - force2 : Type[2]; - lift2 : force2 +(* Non uniform coercions support +record solution2 (S : Type[2]) (s : S) : Type[3] ≝ { + target2 : Type[2]; + result2 : target2 }. -record lock1 (S : Type[1]) (s : S) : Type[2] ≝ { - force1 : Type[1]; - lift1 : force1 +record solution1 (S : Type[1]) (s : S) : Type[2] ≝ { + target1 : Type[1]; + result1 : target1 }. -coercion zzzlift1 : ∀S:Type[1].∀s:S.∀l:lock1 S s. force1 S s l ≝ lift1 - on s : ? to force1 ???. +coercion nonunifcoerc1 : ∀S:Type[1].∀s:S.∀l:solution1 S s. target1 S s l ≝ result1 + on s : ? to target1 ???. -coercion zzzlift2 : ∀S:Type[2].∀s:S.∀l:lock2 S s. force2 S s l ≝ lift2 - on s : ? to force2 ???. +coercion nonunifcoerc2 : ∀S:Type[2].∀s:S.∀l:solution2 S s. target2 S s l ≝ result2 + on s : ? to target2 ???. +*) (* Example of a non uniform coercion declaration @@ -99,9 +100,8 @@ coercion zzzlift2 : ∀S:Type[2].∀s:S.∀l:lock2 S s. force2 S s l ≝ lift2 unification hint 0 ≔ R : setoid; MR ≟ carr R, - lock ≟ mk_lock1 Type[0] MR setoid R + sol ≟ mk_solution1 Type[0] MR setoid R (* ---------------------------------------- *) ⊢ - setoid ≡ force1 ? MR lock. + setoid ≡ target1 ? MR sol. -*) *) \ No newline at end of file -- 2.39.2