1
Есть ли способ распечатать все доступные (существующие в этой точке) символы вместе с их типами в Coq? Я знаю о запросе Print All., но он только показывает символы, определенные в текущем скрипте, за исключением символов, которые могут быть доступны/использованы (импортированы из некоторых библиотек), например. eq_refl : forall (A : Type) (x : A), x = x.Как напечатать все определенные символы в Coq?
Это одно решение, еще один может быть использовать протокол сериализации (например, SerAPI;)), в зависимости от вашего использования. – ejgallego
мой язык пользователя - это python, и я полагаю, что я мог бы взаимодействовать с SerAPI (отправив команду 'Search _.') через json? – Falcon
SerAPI предоставляет более тонкие команды 'query' непосредственно в своем API, поэтому использование поиска не требуется. Это зависит от вашего варианта использования. – ejgallego