Quelle tac2quote_ltac1.ml Sprache: SML

open Ltac2_plugin.Tac2dyn

let wit_ltac1 = Arg.create "ltac1"
let wit_ltac1val = Arg.create "ltac1val"

let val_ltac1 : Geninterp.Val.t Val.tag = Val.create "ltac1"

let ltac1 = Ltac2_plugin.Tac2ffi.repr_ext val_ltac1

Messung V0.5

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

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.