diff options
Diffstat (limited to 'test-suite/success/polymorphism.v')
-rw-r--r-- | test-suite/success/polymorphism.v | 32 |
1 files changed, 31 insertions, 1 deletions
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index 878875bd9..0a58fe89a 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -321,4 +321,34 @@ Definition unwrap' := fun (X : Type) (b : box X) => let (unw) := b in unw. Fail Definition bad : False := TypeNeqSmallType.paradox (unwrap' Type (wrap _ Type)) eq_refl. -End Hurkens'.
\ No newline at end of file +End Hurkens'. + +Module Anonymous. + Set Universe Polymorphism. + + Definition defaultid := (fun x => x) : Type -> Type. + Definition collapseid := defaultid@{_ _}. + Check collapseid@{_}. + + Definition anonid := (fun x => x) : Type -> Type@{_}. + Check anonid@{_}. + + Definition defaultalg := Type : Type. + Definition usedefaultalg := defaultalg@{_ _}. + Check usedefaultalg@{_ _}. + + Definition anonalg := (fun x => x) (Type : Type@{_}). + Check anonalg@{_}. + + Definition unrelated@{i j} := nat. + Definition useunrelated := unrelated@{_ _}. + Check useunrelated@{_ _}. + + Definition inthemiddle@{i j k} := + let _ := defaultid@{i j} in + defaultalg@{k j}. + (* i <= j < k *) + Definition collapsethemiddle := inthemiddle@{i _ j}. + Check collapsethemiddle@{_ _}. + +End Anonymous. |