equal
deleted
inserted
replaced
136 @{text "t\<^isub>1 t\<^isub>2 \<dots> t\<^isub>n"} and right hand side @{text t}). |
136 @{text "t\<^isub>1 t\<^isub>2 \<dots> t\<^isub>n"} and right hand side @{text t}). |
137 Code generation aims to turn code equations |
137 Code generation aims to turn code equations |
138 into a functional program. This is achieved by three major |
138 into a functional program. This is achieved by three major |
139 components which operate sequentially, i.e. the result of one is |
139 components which operate sequentially, i.e. the result of one is |
140 the input |
140 the input |
141 of the next in the chain, see diagram \ref{fig:arch}: |
141 of the next in the chain, see figure \ref{fig:arch}: |
142 |
142 |
143 \begin{itemize} |
143 \begin{itemize} |
144 |
144 |
145 \item Starting point is a collection of raw code equations in a |
145 \item Starting point is a collection of raw code equations in a |
146 theory; due to proof irrelevance it is not relevant where they |
146 theory; due to proof irrelevance it is not relevant where they |