matita/matita/lib/extraction.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "arithmetics/nat.ma".
  16
  17 (*BUG: kind signatures in type declarations*)
  18
  19 axiom test1: Type[1].
  20
  21 axiom test2: Type[1] → Type[1].
  22
  23 axiom test3: Prop → Type[1] → CProp[1] → Type[1] → Type[2].
  24
  25 (* not in F_omega ? *)
  26 axiom test4: ∀A:Type[1]. A → ∀B:Type[1]. B → ∀C:Prop. C → Type[1].
  27
  28 axiom test5: (Type[1] → Type[1]) → Type[1].
  29
  30 (* no content *)
  31 axiom test6: Type[1] → Prop.
  32
  33 definition dtest1: Type[1] ≝ nat → nat.
  34
  35 definition dtest2: Type[2] ≝ ∀A:Type[1]. A → A.
  36
  37 definition dtest3: Type[1] → Type[1] ≝ λA:Type[1]. A → A.
  38
  39 definition dtest4: Type[1] → Type[1] ≝ λA:Type[1].dtest3 A.
  40
  41 definition dtest5: Type[1] → Type[1] ≝ dtest3.
  42
  43 definition dtest6: Type[1] ≝ dtest3 nat.
  44
  45 (* no content *)
  46 definition dtest7: Prop ≝ True → True.
  47
  48 (* no content *)
  49 definition dtest8: Type[1] ≝ dtest3 True.
  50
  51 (* no content *)
  52 definition dtest9: Type[1] ≝ dtest3 Prop.
  53
  54 definition dtest10: Type[1] → Type[1] → Type[1] ≝ λX,Y.X.
  55
  56 (*BUG: a' vs a''*)
  57 definition dtest11: Type[1] → nat → Type[1] → Type[1] ≝ λ_:Type[1].λ_:nat.λX:Type[1]. X → nat → test1.
  58
  59 definition dtest12 ≝ λ_:Type[1].λ_:nat.λX:Type[1]. X → nat → test1.
  60
  61 definition dtest13 ≝ dtest3 nat → dtest3 True → dtest3 Prop → nat.
  62
  63 definition dtest14 ≝ λX:Type[2]. X → X.
  64
  65 (*FEATURE: type the forall bound variables*)
  66 definition dtest15 ≝ ∀T:Type[1] → Type[1]. T nat → T nat.
  67
  68 definition dtest16 ≝ ∀T:Type[1]. T → nat.
  69
  70 definition dtest17 ≝ ∀T:dtest14 Type[1]. T nat → dtest14 nat → dtest14 nat.
  71
  72 definition dtest18 ≝ λA,B:Type[0].λn:nat.λC:Type[0].A.
  73
  74 definition dtest19 ≝ dtest18 nat True O nat → dtest18 nat nat O nat.
  75
  76 definition dtest20 ≝ test5 test2.
  77
  78 (*BUG: lambda-lift the inner declaration;
  79   to be traced, raises NotInFOmega; why? *)
  80 definition dtest21 ≝ test5 (λX:Type[1].X).
  81
  82 definition ttest1 ≝ λx:nat.x.
  83
  84 (*BUG: clash of name due to capitalisation*)
  85 definition Ttest1 ≝ λx:nat.x.
  86
  87 (*BUG: Failure nth*)
  88 definition ttest2 ≝ λT:Type[1].λx:T.x.