diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 18:33:25 +0100 |
commit | 1b92c226e563643da187b8614d5888dc4855eb43 (patch) | |
tree | c4c3d204b36468b58cb71050ba95f06b8dd7bc2e /test-suite/success/vm_univ_poly.v | |
parent | 7c9b0a702976078b813e6493c1284af62a3f093c (diff) |
Imported Upstream version 8.6
Diffstat (limited to 'test-suite/success/vm_univ_poly.v')
-rw-r--r-- | test-suite/success/vm_univ_poly.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/test-suite/success/vm_univ_poly.v b/test-suite/success/vm_univ_poly.v index 58fa3974..62df96c0 100644 --- a/test-suite/success/vm_univ_poly.v +++ b/test-suite/success/vm_univ_poly.v @@ -38,8 +38,8 @@ Definition _4 : sumbool_copy x = x := (* Polymorphic Inductive Types *) Polymorphic Inductive poption@{i} (T : Type@{i}) : Type@{i} := -| PSome : T -> poption@{i} T -| PNone : poption@{i} T. +| PSome : T -> poption T +| PNone : poption T. Polymorphic Definition poption_default@{i} {T : Type@{i}} (p : poption@{i} T) (x : T) : T := match p with @@ -49,7 +49,7 @@ Polymorphic Definition poption_default@{i} {T : Type@{i}} (p : poption@{i} T) (x Polymorphic Inductive plist@{i} (T : Type@{i}) : Type@{i} := | pnil -| pcons : T -> plist@{i} T -> plist@{i} T. +| pcons : T -> plist T -> plist T. Arguments pnil {_}. Arguments pcons {_} _ _. @@ -59,7 +59,7 @@ Polymorphic Definition pmap@{i j} fix pmap (ls : plist@{i} T) : plist@{j} U := match ls with | @pnil _ => @pnil _ - | @pcons _ l ls => @pcons@{j} U (f l) (pmap@{i j} ls) + | @pcons _ l ls => @pcons@{j} U (f l) (pmap ls) end. Universe Ubool. @@ -75,7 +75,7 @@ Eval vm_compute in pmap (fun x => x -> Type) (pcons tbool (pcons (plist tbool) p Polymorphic Inductive Tree@{i} (T : Type@{i}) : Type@{i} := | Empty -| Branch : plist@{i} (Tree@{i} T) -> Tree@{i} T. +| Branch : plist@{i} (Tree T) -> Tree T. Polymorphic Definition pfold@{i u} {T : Type@{i}} {U : Type@{u}} (f : T -> U -> U) := @@ -111,7 +111,7 @@ Polymorphic Fixpoint repeat@{i} {T : Type@{i}} (n : nat@{i}) (v : T) : plist@{i} Polymorphic Fixpoint big_tree@{i} (n : nat@{i}) : Tree@{i} nat@{i} := match n with | O => @Empty nat@{i} - | S n' => Branch@{i} nat@{i} (repeat@{i} n' (big_tree@{i} n')) + | S n' => Branch@{i} nat@{i} (repeat@{i} n' (big_tree n')) end. Eval compute in height (big_tree (S (S (S O)))). |