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

Last change on this file since 259 was 249, checked in by mulligan, 10 years ago

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