Quelle BDD_Code.thy

Sprache: Isabelle

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]

export_code open iteci_lu notci andci orci nandci norci biimpci xorci ifci tci fci tautci emptyci graphifyci litci eqci checking Haskell

end

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.9 Sekunden (vorverarbeitet am 2026-06-10) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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.