Towards an extraction of CaPriCon terms to functional programs CaPriCon is now endowed with a new 'axiom' builtin, which produces an opaque value of an arbitrary type, meant to represent an external function (such as an OCaml constructor or type name) which will be supplied by the runtime after extraction. Said extraction can then proceed by identifying inductive types within the term to extract, and defining an axiom for each of those types' constructors. Then, it can substitute each occurrence of an inductive value with its equivalent using the now-defined inductive axioms, and finally erase the extraneous type information to produce an abstract algebraic functional representation of the initial term. More in the next release...