1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "arithmetics/nat.ma".
17 (*BUG: kind signatures in type declarations*)
21 axiom test2: Type[1] → Type[1].
23 axiom test3: Prop → Type[1] → CProp[1] → Type[1] → Type[2].
25 (* not in F_omega ? *)
26 axiom test4: ∀A:Type[1]. A → ∀B:Type[1]. B → ∀C:Prop. C → Type[1].
28 axiom test5: (Type[1] → Type[1]) → Type[1].
31 axiom test6: Type[1] → Prop.
33 definition dtest1: Type[1] ≝ nat → nat.
35 definition dtest2: Type[2] ≝ ∀A:Type[1]. A → A.
37 definition dtest3: Type[1] → Type[1] ≝ λA:Type[1]. A → A.
39 definition dtest4: Type[1] → Type[1] ≝ λA:Type[1].dtest3 A.
41 definition dtest5: Type[1] → Type[1] ≝ dtest3.
43 definition dtest6: Type[1] ≝ dtest3 nat.
46 definition dtest7: Prop ≝ True → True.
49 definition dtest8: Type[1] ≝ dtest3 True.
52 definition dtest9: Type[1] ≝ dtest3 Prop.
54 definition dtest10: Type[1] → Type[1] → Type[1] ≝ λX,Y.X.
57 definition dtest11: Type[1] → nat → Type[1] → Type[1] ≝ λ_:Type[1].λ_:nat.λX:Type[1]. X → nat → test1.
59 definition dtest12 ≝ λ_:Type[1].λ_:nat.λX:Type[1]. X → nat → test1.
61 definition dtest13 ≝ dtest3 nat → dtest3 True → dtest3 Prop → nat.
63 definition dtest14 ≝ λX:Type[2]. X → X.
65 (*FEATURE: type the forall bound variables*)
66 definition dtest15 ≝ ∀T:Type[1] → Type[1]. T nat → T nat.
68 definition dtest16 ≝ ∀T:Type[1]. T → nat.
70 definition dtest17 ≝ ∀T:dtest14 Type[1]. T nat → dtest14 nat → dtest14 nat.
72 definition dtest18 ≝ λA,B:Type[0].λn:nat.λC:Type[0].A.
74 definition dtest19 ≝ dtest18 nat True O nat → dtest18 nat nat O nat.
76 definition dtest20 ≝ test5 test2.
78 (*BUG: lambda-lift the inner declaration;
79 to be traced, raises NotInFOmega; why? *)
80 definition dtest21 ≝ test5 (λX:Type[1].X).
82 definition ttest1 ≝ λx:nat.x.
84 (*BUG: clash of name due to capitalisation*)
85 definition Ttest1 ≝ λx:nat.x.
88 definition ttest2 ≝ λT:Type[1].λx:T.x.