]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/tests/ng_commands.ma
splitting files
[helm.git] / matita / matita / tests / ng_commands.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 "ng_pts.ma".
16
17 ndefinition thesis0: ∀A:Type.Type ≝ λA. A → A.
18
19 ndefinition thesis: ∀A:Type.Type ≝ λA. ?.
20  napply (A → A);
21 nqed.
22
23 ntheorem foo: ∀A:Type.thesis A.#A;#x;napply x;
24 nqed.
25
26 ntheorem goo: ∀A:Type.A → A. #A; napply (foo ?);
27 nqed.
28
29 naxiom NP: Prop.
30
31 ndefinition Q: Prop ≝ NP.
32
33 include "nat/nat.ma".
34
35 nlet rec nzero (n:nat) : nat ≝
36  match n with
37   [ O ⇒ O
38   | S m ⇒ nzero m].
39
40 ntheorem nzero_ok: nzero (S (S O)) = O.
41  napply (refl_eq ? O);
42 nqed.
43
44 naxiom DT: nat → Type.
45 naxiom dt: ∀n. DT n.
46
47 ninductive nnat (n: nat) (A:DT n): Type ≝
48    nO: nnat n A
49  | nS: mat n A → mat n A → nnat n A
50 with mat: Type ≝ 
51  |mS : nnat n A → mat n A.
52
53 nlet rec nnzero (n:nnat 0 (dt ?)) : nnat 0 (dt ?) ≝
54  match n return ? with
55   [ nO ⇒ nO 0 (dt ?)
56   | nS m _ ⇒ nmzero m ]
57 and nmzero (m:mat 0 (dt ?)) : nnat 0 (dt ?) ≝ 
58  match m return ? with
59  [ mS n ⇒ nnzero n ].
60
61 nrecord pair (n: nat) (x: DT n) (label: Type): Type ≝
62  { lbl:label; l: pair n x label; r: pair n x label}.