equal
deleted
inserted
replaced
12 Multiple nested quotations and anti-quotations -- basically a |
12 Multiple nested quotations and anti-quotations -- basically a |
13 generalized version of de-Bruijn representation. |
13 generalized version of de-Bruijn representation. |
14 *} |
14 *} |
15 |
15 |
16 syntax |
16 syntax |
17 "_quote" :: "'b => ('a => 'b)" ("\<guillemotleft>_\<guillemotright>" [0] 1000) |
17 "_quote" :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("\<guillemotleft>_\<guillemotright>" [0] 1000) |
18 "_antiquote" :: "('a => 'b) => 'b" ("\<acute>_" [1000] 1000) |
18 "_antiquote" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b" ("\<acute>_" [1000] 1000) |
19 |
19 |
20 parse_translation {* |
20 parse_translation {* |
21 let |
21 let |
22 fun antiquote_tr i (Const (@{syntax_const "_antiquote"}, _) $ |
22 fun antiquote_tr i (Const (@{syntax_const "_antiquote"}, _) $ |
23 (t as Const (@{syntax_const "_antiquote"}, _) $ _)) = skip_antiquote_tr i t |
23 (t as Const (@{syntax_const "_antiquote"}, _) $ _)) = skip_antiquote_tr i t |
41 term "\<guillemotleft>\<acute>(f w) + \<acute>x\<guillemotright>" |
41 term "\<guillemotleft>\<acute>(f w) + \<acute>x\<guillemotright>" |
42 term "\<guillemotleft>f \<acute>x \<acute>y z\<guillemotright>" |
42 term "\<guillemotleft>f \<acute>x \<acute>y z\<guillemotright>" |
43 |
43 |
44 text {* advanced examples *} |
44 text {* advanced examples *} |
45 term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>x + \<acute>y\<guillemotright>\<guillemotright>" |
45 term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>x + \<acute>y\<guillemotright>\<guillemotright>" |
46 term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>x + \<acute>y\<guillemotright> o \<acute>f\<guillemotright>" |
46 term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>x + \<acute>y\<guillemotright> \<circ> \<acute>f\<guillemotright>" |
47 term "\<guillemotleft>\<acute>(f o \<acute>g)\<guillemotright>" |
47 term "\<guillemotleft>\<acute>(f \<circ> \<acute>g)\<guillemotright>" |
48 term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>(f o \<acute>g)\<guillemotright>\<guillemotright>" |
48 term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>(f \<circ> \<acute>g)\<guillemotright>\<guillemotright>" |
49 |
49 |
50 end |
50 end |