section‹Code export› theory BDD_Code imports Level_Collapse begin
text‹For convenience reasons, the code export is in a separate theory. For Haskell, we only have to reactivate the original equation for @{term blit}. Other languages might need an implementation for it.›
lemma [code del]: "blit src si dst di len = blit' src (integer_of_nat si) dst (integer_of_nat di) (integer_of_nat len)"by (simp add: blit'_def) declare blit_def[code]
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
