equal
deleted
inserted
replaced
99 text \<open>Some syntactic sugar for summing a function over a list:\<close> |
99 text \<open>Some syntactic sugar for summing a function over a list:\<close> |
100 syntax (ASCII) |
100 syntax (ASCII) |
101 "_sum_list" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10) |
101 "_sum_list" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10) |
102 syntax |
102 syntax |
103 "_sum_list" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10) |
103 "_sum_list" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10) |
|
104 syntax_consts |
|
105 "_sum_list" == sum_list |
104 translations \<comment> \<open>Beware of argument permutation!\<close> |
106 translations \<comment> \<open>Beware of argument permutation!\<close> |
105 "\<Sum>x\<leftarrow>xs. b" == "CONST sum_list (CONST map (\<lambda>x. b) xs)" |
107 "\<Sum>x\<leftarrow>xs. b" == "CONST sum_list (CONST map (\<lambda>x. b) xs)" |
106 |
108 |
107 context |
109 context |
108 includes lifting_syntax |
110 includes lifting_syntax |
596 |
598 |
597 syntax (ASCII) |
599 syntax (ASCII) |
598 "_prod_list" :: "pttrn => 'a list => 'b => 'b" ("(3PROD _<-_. _)" [0, 51, 10] 10) |
600 "_prod_list" :: "pttrn => 'a list => 'b => 'b" ("(3PROD _<-_. _)" [0, 51, 10] 10) |
599 syntax |
601 syntax |
600 "_prod_list" :: "pttrn => 'a list => 'b => 'b" ("(3\<Prod>_\<leftarrow>_. _)" [0, 51, 10] 10) |
602 "_prod_list" :: "pttrn => 'a list => 'b => 'b" ("(3\<Prod>_\<leftarrow>_. _)" [0, 51, 10] 10) |
|
603 syntax_consts |
|
604 "_prod_list" \<rightleftharpoons> prod_list |
601 translations \<comment> \<open>Beware of argument permutation!\<close> |
605 translations \<comment> \<open>Beware of argument permutation!\<close> |
602 "\<Prod>x\<leftarrow>xs. b" \<rightleftharpoons> "CONST prod_list (CONST map (\<lambda>x. b) xs)" |
606 "\<Prod>x\<leftarrow>xs. b" \<rightleftharpoons> "CONST prod_list (CONST map (\<lambda>x. b) xs)" |
603 |
607 |
604 context |
608 context |
605 includes lifting_syntax |
609 includes lifting_syntax |