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は別の仮説/変数で同じブランチをやり直そうとするため、そのような仮説/変数はすべて印刷されてしまいます。今、第2ブランチ| _ => idtacは、戦術が最終的に成功することを確認することです。このブランチが存在しない場合、戦術はエラーで失敗し、エラーを印刷すると、Coqは以前に印刷した情報を消去します。

Answer 3

近似値を検索することができます。あなたはできる：

Search $Type. 

結果とタイプ$Typeを得る。例えば、

Search nat -(forall _, _). 

はタイプnatのすべての条項が表示されます。

Search Set -(forall _, _). 

はタイプSetのすべての非機能的用語を表示します。 SearchPatternは同様の機能を提供するはずですが、わかりません。 Ssreflect検索でそれ以上のことができます。