equal
deleted
inserted
replaced
|
1 |
|
2 (* Author: Florian Haftmann, TU Muenchen *) |
|
3 |
|
4 header {* Pervasive test of code generator using pretty literals *} |
|
5 |
|
6 theory Generate_Pretty |
|
7 imports Candidates_Pretty |
|
8 begin |
|
9 |
|
10 lemma [code, code del]: "nat_of_char = nat_of_char" .. |
|
11 lemma [code, code del]: "char_of_nat = char_of_nat" .. |
|
12 lemma [code, code del]: "(less_eq :: char \<Rightarrow> _) = less_eq" .. |
|
13 lemma [code, code del]: "(less :: char \<Rightarrow> _) = less" .. |
|
14 |
|
15 export_code * in SML module_name Code_Test |
|
16 in OCaml module_name Code_Test file - |
|
17 in Haskell file - |
|
18 in Scala file - |
|
19 |
|
20 end |