| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Hello_World/ (Archive of formal Proofs Version 2026-5©) Datei vom 31.4.2026 mit Größe 1 kB |
|
Quelle HelloWorld.thy Sprache: Isabelle |
|||||||||||||||||||||||||
|
theory HelloWorld imports IO begin section‹Hello, World!› text‹ The idea of a term‹main :: unit io› function is that, upon start of your program handed a value of type typ‹🌐›. You can pass this world through your code and mo Be careful with the typ‹🌐›, it's the only one we have. text‹The main function, defined in Isabelle. It should have the right type in Ha definition main :: "unit io" where "main ≡ do { _ ← println (STR ''Hello World! What is your name?''); name ← getLine; println (STR ''Hello, '' + name + STR ''!'') }" section‹Generating Code› text‹Checking that the generated code compiles.› export_code main checking Haskell? SML (*<*) setup ‹ val parser = Scan.repeat (Args.const {proper = true, strict = true}) -- Scan.lift (🚫‹in› |-- Parse.name -- (🚫‹module_name› |-- Parse.name)) fun action ctxt (consts, (target, module)) = Code_Target.produce_code ctxt false consts target module NONE [] |> fst |> map (Bytes.content o snd) |> String.concatWith "\n" Document_Output.antiquotation_verbatim @{binding code} parser action › (*>*) subsection‹Haskell› text‹The generated code in Haskell (including the prelude) is shown below.› text_raw‹@{code main in Haskell module_name HelloWorld}› subsection‹SML› text‹The generated code in SML (including the prelude) is shown below.› text_raw‹@{code main in SML module_name HelloWorld}› end
¤ Dauer der Verarbeitung: 0.6 Sekunden ¤*© Formatika GbR, Deutschland |
|
||||||||||||||||||||||||
2026-11-01