Coq: Показать все термины в типе или типах в юниверсе в среде

Question

Есть ли способ отображать все термины типа или всех типов в юниверсе в окружающей среде?

Print Set. (*Syntax error: 'Firstorder' 'Solver' expected after 'Print' (in [vernac:command]).*) 

Answer 1

Нет, таких функций в Coq нет. Print будет отображаться только телом данного термина, например:

Print plus. 
plus = 
fix plus (n m : nat) {struct n} : nat := 
    match n with 
    | 0 => m 
    | S p => S (plus p m) 
    end 
    : nat -> nat -> nat 

Argument scopes are [nat_scope nat_scope] 

Answer 2

Следующие определенного пользователь тактик может сделать именно это, если средой вы имеете в виду доказательства среды.

Ltac printInType t := 
    match goal with 
    | [ H : t |- _ ] => 
     idtac H; fail 
    | _ => idtac 
    end 
. 

Theorem test : forall n m, n + m = m + n. 
Proof. 
    intros. 
    printInType nat. 
    (* prints in the Message window: 
    m 
    n 
    *) 
    printInType Set. 
    (* prints nothing 
    because nat for instance is not explicitely in the proof environment *) 

Что она делает именно это проходит через доказательство среды и находит гипотезу или переменную, которая имеет тип аргумента t. idtac H отпечатывает его, затем ветка терпит неудачу из-за тактики fail. Теперь Coq снова пытается использовать одну и ту же ветвь по другой гипотезе/переменной, поэтому все такие гипотезы/переменные в конечном итоге печатаются. Теперь вторая ветка | _ => idtac - это просто убедиться, что тактика в конечном итоге преуспеет. Если этой ветви не было, тактика выйдет из строя с ошибкой, а при печати ошибки Coq удалит ранее опубликованную информацию.

Answer 3

Вы можете использовать поиск в близи к этому. Вы можете сделать:

Search $Type. 

и получить результаты с типом $Type. Например,

Search nat -(forall _, _). 

покажет все условия типа nat.

Search Set -(forall _, _). 

Показать все нефункциональные термины типа Set. SearchPattern должен предлагать аналогичные функции, но я не уверен. Ssreflect поиск может сделать это и многое другое.