diff options
Diffstat (limited to 'examples/unix/Char.gf')
| -rw-r--r-- | examples/unix/Char.gf | 51 |
1 files changed, 51 insertions, 0 deletions
diff --git a/examples/unix/Char.gf b/examples/unix/Char.gf new file mode 100644 index 000000000..f10284587 --- /dev/null +++ b/examples/unix/Char.gf @@ -0,0 +1,51 @@ +abstract Char = { + + cat + [Chr] {1} ; Chr ; Letter ; + + fun + C_dot : Chr ; + C_pipe : Chr ; + C_hyphen : Chr ; + CSmall : Letter -> Chr ; + CCap : Letter -> Chr ; + CC : Letter -> Chr ; + + CDig_0 : Chr ; + CDig_1 : Chr ; + CDig_2 : Chr ; + CDig_3 : Chr ; + CDig_4 : Chr ; + CDig_5 : Chr ; + CDig_6 : Chr ; + CDig_7 : Chr ; + CDig_8 : Chr ; + CDig_9 : Chr ; + + L_a : Letter ; + L_b : Letter ; + L_c : Letter ; + L_d : Letter ; + L_e : Letter ; + L_f : Letter ; + L_g : Letter ; + L_h : Letter ; + L_i : Letter ; + L_j : Letter ; + L_k : Letter ; + L_l : Letter ; + L_m : Letter ; + L_n : Letter ; + L_o : Letter ; + L_p : Letter ; + L_q : Letter ; + L_r : Letter ; + L_s : Letter ; + L_t : Letter ; + L_u : Letter ; + L_v : Letter ; + L_w : Letter ; + L_x : Letter ; + L_y : Letter ; + L_z : Letter ; +} |