diff options
author | 2017-05-05 15:36:58 +0200 | |
---|---|---|
committer | 2017-05-05 15:36:58 +0200 | |
commit | 1b4b828c3045263aee55ac19e7b9ba45a4743af2 (patch) | |
tree | 73f7c9ed6210bc0449e0974d9dd20c79199718a1 /test-suite/success | |
parent | 773d95f915996b581b7ea82d9193197649c951a0 (diff) | |
parent | 4361c1ed9ac5646055f9f0eecc4a003d720c1994 (diff) |
Merge PR#544: Anonymous universes
Diffstat (limited to 'test-suite/success')
-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..66ff55edc 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 := (fun x : Type => x) (Type : Type). + Definition usedefaultalg := defaultalg@{_ _ _}. + Check usedefaultalg@{_ _}. + + Definition anonalg := (fun x : Type@{_} => 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 + anonalg@{k j}. + (* i <= j < k *) + Definition collapsethemiddle := inthemiddle@{i _ j}. + Check collapsethemiddle@{_ _}. + +End Anonymous. |