diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /test-suite/success/AdvancedCanonicalStructure.v | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'test-suite/success/AdvancedCanonicalStructure.v')
-rw-r--r-- | test-suite/success/AdvancedCanonicalStructure.v | 28 |
1 files changed, 18 insertions, 10 deletions
diff --git a/test-suite/success/AdvancedCanonicalStructure.v b/test-suite/success/AdvancedCanonicalStructure.v index 97cf316c..d819dc47 100644 --- a/test-suite/success/AdvancedCanonicalStructure.v +++ b/test-suite/success/AdvancedCanonicalStructure.v @@ -47,6 +47,24 @@ Goal forall a1 a2, eqA (plusA a1 zeroA) a2. change (eqB (plusB (phi a1) zeroB) (phi a2)). Admitted. +Variable foo : A -> Type. + +Definition local0 := fun (a1 : A) (a2 : A) (a3 : A) => + (eq_refl : plusA a1 (plusA zeroA a2) = ia _). +Definition local1 := + fun (a1 : A) (a2 : A) (f : A -> A) => + (eq_refl : plusA a1 (plusA zeroA (f a2)) = ia _). + +Definition local2 := + fun (a1 : A) (f : A -> A) => + (eq_refl : (f a1) = ia _). + +Goal forall a1 a2, eqA (plusA a1 zeroA) a2. + intros a1 a2. + refine (eq_img _ _ _). +change (eqB (plusB (phi a1) zeroB) (phi a2)). +Admitted. + End group_morphism. Open Scope type_scope. @@ -129,13 +147,3 @@ Admitted. Check L : abs _ . End type_reification. - - - - - - - - - - |