1
Gibt es eine Möglichkeit, alle verfügbaren (zu diesem Zeitpunkt vorhandenen) Symbole zusammen mit ihren Typen in Coq zu drucken? Ich weiß über die Print All. Abfrage, aber es scheint nur die im aktuellen Skript definierten Symbole zu zeigen, ausgenommen Symbole, auf die zugegriffen werden kann (die aus einigen Bibliotheken importiert werden), z. eq_refl : forall (A : Type) (x : A), x = x.Wie alle definierten Symbole in Coq gedruckt werden?
, dass eine Lösung ist, sein ein anderer kann eine Serialisierung Protokoll zu verwenden (wie Serapi;)), auf Ihren Anwendungsfall abhängig. – ejgallego
meine Benutzersprache ist Python und ich stelle mir vor, dass ich mit SerAPI (Senden eines Befehls 'Search _.) über Json interagieren könnte? – Falcon
SerAPI bietet mehr feinkörnige query-Befehle direkt in seiner API, so dass die Verwendung der Suche nicht notwendig ist. Es hängt davon ab, was dein Anwendungsfall ist. – ejgallego