equal
deleted
inserted
replaced
1018 \item[@{text "t."}\hthm{rec} @{text "[simp, code]"}\rm:] ~ \\ |
1018 \item[@{text "t."}\hthm{rec} @{text "[simp, code]"}\rm:] ~ \\ |
1019 @{thm list.rec(1)[no_vars]} \\ |
1019 @{thm list.rec(1)[no_vars]} \\ |
1020 @{thm list.rec(2)[no_vars]} \\ |
1020 @{thm list.rec(2)[no_vars]} \\ |
1021 (The @{text "[code]"} attribute is set by the @{text code} plugin, |
1021 (The @{text "[code]"} attribute is set by the @{text code} plugin, |
1022 Section~\ref{ssec:code-generator}.) |
1022 Section~\ref{ssec:code-generator}.) |
|
1023 |
|
1024 \item[@{text "t."}\hthm{rec_o_map}\rm:] ~ \\ |
|
1025 @{thm list.rec_o_map[no_vars]} |
1023 |
1026 |
1024 \item[@{text "t."}\hthm{rec_transfer}\rm:] ~ \\ |
1027 \item[@{text "t."}\hthm{rec_transfer}\rm:] ~ \\ |
1025 @{thm list.rec_transfer[no_vars]} |
1028 @{thm list.rec_transfer[no_vars]} |
1026 |
1029 |
1027 \end{description} |
1030 \end{description} |
2858 @{thm list.size(1)[no_vars]} \\ |
2861 @{thm list.size(1)[no_vars]} \\ |
2859 @{thm list.size(2)[no_vars]} \\ |
2862 @{thm list.size(2)[no_vars]} \\ |
2860 @{thm list.size(3)[no_vars]} \\ |
2863 @{thm list.size(3)[no_vars]} \\ |
2861 @{thm list.size(4)[no_vars]} |
2864 @{thm list.size(4)[no_vars]} |
2862 |
2865 |
2863 \item[@{text "t."}\hthm{rec_o_map}\rm:] ~ \\ |
|
2864 @{thm list.rec_o_map[no_vars]} |
|
2865 |
|
2866 \item[@{text "t."}\hthm{size_o_map}\rm:] ~ \\ |
2866 \item[@{text "t."}\hthm{size_o_map}\rm:] ~ \\ |
2867 @{thm list.size_o_map[no_vars]} |
2867 @{thm list.size_o_map[no_vars]} |
2868 |
2868 |
2869 \end{description} |
2869 \end{description} |
2870 \end{indentblock} |
2870 \end{indentblock} |