source: Deliverables/D4.1/Matita/Char.ma @ 475

Last change on this file since 475 was 432, checked in by mulligan, 9 years ago

Removed Plogic/

File size: 604 bytes
Line 
1include "logic/pts.ma".
2
3(*
4ninductive Char: Type[0] ≝
5  a: Char
6| b: Char
7| c: Char
8| d: Char
9| e: Char
10| f: Char
11| g: Char
12| h: Char
13| i: Char
14| j: Char
15| k: Char
16| l: Char
17| m: Char
18| n: Char
19| o: Char
20| p: Char
21| q: Char
22| r: Char
23| s: Char
24| t: Char
25| u: Char
26| v: Char
27| w: Char
28| x: Char
29| y: Char
30| z: Char
31| A: Char
32| B: Char
33| C: Char
34| D: Char
35| E: Char
36| F: Char
37| G: Char
38| H: Char
39| I: Char
40| J: Char
41| K: Char
42| L: Char
43| M: Char
44| N: Char
45| O: Char
46| P: Char
47| Q: Char
48| R: Char
49| S: Char
50| T: Char
51| U: Char
52| V: Char
53| W: Char
54| X: Char
55| Y: Char
56| Z: Char.
57*)
58
59naxiom Char: Type[0].
Note: See TracBrowser for help on using the repository browser.