products/sources/formale Sprachen/Coq/doc/plugin_tutorial/tuto0/src image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei:   Sprache: Unknown

Columbo aufrufen.mlg zum Wurzelverzeichnis wechselnShell {Shell[45] Isabelle[83] Cobol[109]}Datei anzeigen

DECLARE PLUGIN "tuto0_plugin"

{

open Pp
open Ltac_plugin

}

VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY
| [ "HelloWorld" ] -> { Feedback.msg_notice (strbrk Tuto0_main.message) }
END

TACTIC EXTEND hello_world_tactic
| [ "hello_world" ] ->
  { let _ = Feedback.msg_notice (str Tuto0_main.message) in
    Tacticals.New.tclIDTAC }
END

[ Original von:0.65Diese Quellcodebibliothek enthält Beispiele in vielen Programmiersprachen. Man kann per Verzeichnistruktur darin navigieren. Der Code wird farblich markiert angezeigt.  ]