1
利用可能な（その時点で存在している）すべてのシンボルをCoqのタイプと共に印刷する方法はありますか？私はPrint All.クエリについて知っていますが、現在のスクリプトで定義されているシンボルを表示するように見えますが、アクセス可能/使用可能なシンボルは除外されています。 eq_refl : forall (A : Type) (x : A), x = x。私は一つの解決見つけたと思うCoqに定義されたシンボルをすべて印刷するには？
一つの解決策だ、もう一つは、（SerAPIなど）直列化プロトコルを使用することであってもよいです。 – ejgallego
私のユーザ言語はPythonです.Json経由でSerAPI（ 'Search _.'コマンドを送る）とやりとりすることができると思いますか？ – Falcon
SerAPIはAPIでより細かい 'query'コマンドを直接提供するので、検索は不要です。それはあなたのユースケースがあなたのものであるかによって異なります。 – ejgallego