(* Title: HOL/Library/IArray.thy Author: Tobias Nipkow, TU Muenchen Author: Jose Divasón <jose.divasonm at unirioja.es> Author: Jesús Aransay <jesus-maria.aransay at unirioja.es> *) section ‹Immutable Arrays with Code Generation› theory IArray imports Main begin subsection ‹Fundamental operations› text ‹Immutable arrays are lists wrapped up in an additional constructor. There are no update operations. Hence code generation can safely implement this type by efficient target language arrays. Currently only SML is provided. Could be extended to other target languages and more operations.› context begin