\[\begin{split}\newcommand{\alors}{\textsf{then}} \newcommand{\alter}{\textsf{alter}} \newcommand{\as}{\kw{as}} \newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} \newcommand{\bool}{\textsf{bool}} \newcommand{\case}{\kw{case}} \newcommand{\conc}{\textsf{conc}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\conshl}{\textsf{cons\_hl}} \newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\EqSt}{\textsf{EqSt}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\false}{\textsf{false}} \newcommand{\filter}{\textsf{filter}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\from}{\textsf{from}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\haslength}{\textsf{has\_length}} \newcommand{\hd}{\textsf{hd}} \newcommand{\ident}{\textsf{ident}} \newcommand{\In}{\kw{in}} \newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)} \newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\lb}{\lambda} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\Nat}{\mathbb{N}} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\Prod}{\textsf{prod}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\si}{\textsf{if}} \newcommand{\sinon}{\textsf{else}} \newcommand{\Sort}{\cal S} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\true}{\textsf{true}} \newcommand{\Type}{\textsf{Type}} \newcommand{\unfold}{\textsf{unfold}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\cal W\!F}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\cal W\!F}(#2)} \newcommand{\WFTWOLINES}[2]{{\cal W\!F}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \newcommand{\zeros}{\textsf{zeros}} \end{split}\]

型クラス

この章では型クラスに関連したコマンドのクイックリファレンスを提供します。実際の型クラスの導入については、システムについての説明が [SO08] にあることに加え Haskell での型クラスについての論文も応用することが出来ます。

クラスとインスタンスの宣言

クラスとインスタンスの宣言の構文は Coq のレコード構文と同じです:

Class Id ( p\(_{1}\) : t\(_{1}\) ) ⋯ ( p\(_{n}\) : t\(_{n}\) ) [: sort] := { f\(_{1}\) : u\(_{1}\) ; ⋮ f\(_{m}\) : u\(_{m}\) }.

Instance ident : Id p\(_{1}\) ⋯ p\(_{n}\) := { f\(_{1}\) := t\(_{1}\) ; ⋮ f\(_{m}\) := t\(_{m}\) }.

変数 p\(_{i}\) : t\(_{i}\) はクラスの パラメータ と呼ばれ、f\(_{i}\) : t\(_{i}\) は メソッド と呼ばれます。各クラス定義は対応するレコード宣言を生みだし、各インスタンスは標準の定義でありその名前は ident で与えられ、型はレコード型のインスタンス化です。

この章の残りでは以下の例示クラスを使います:

Class EqDec (A : Type) := {   eqb : A -> A -> bool ;   eqb_leibniz : forall x y, eqb x y = true -> x = y }.

EqDec is defined eqb is defined eqb_leibniz is defined

このクラスは真偽値等値性テストを実装しており、それはある種の型上で Leibniz 等値性と互換性があります。実装例の一つは:

Instance unit_EqDec : EqDec unit :=  { eqb x y := true ;    eqb_leibniz x y H :=          match x, y return x = y with tt, tt => eq_refl tt end }.

unit_EqDec is defined

インスタンス宣言の中で全てのメンバを与えない場合、Coq は証明モードに入りユーザが残りのフィールドの住民の構築を要求されます。例えば:

Instance eq_bool : EqDec bool := { eqb x y := if x then y else negb y }.

1 subgoal ============================ forall x y : bool, (if x then y else negb y) = true -> x = y

Proof.

intros x y H.

1 subgoal x, y : bool H : (if x then y else negb y) = true ============================ x = y

destruct x ; destruct y ; (discriminate || reflexivity).

No more subgoals.

Defined.

eq_bool is defined

Instance の証明の透過性よって決まる全てのフィールドの透過性に注意するべきです。替わりに Program Instance という類型コマンドを使うことが出来、これは証明課題の扱いについてより豊富な機能を持っています。

クラスの束縛

一度型クラスが宣言されると、それをクラス束縛子の中で使うことができます:

Definition neqb {A} {eqa : EqDec A} (x y : A) := negb (eqb x y).

neqb is defined

クラスメソッドを呼ぶとき、ある制約が生成され、それは適切なインスタンスが見つかる文脈の中でのみ充足されます。上の例では、制約 EqDec A が生成され eqa : EqDec A によって充足されます。制約を充足するものが見つからない場合は、エラーが起きます:

Fail Definition neqb' (A : Type) (x y : A) := negb (eqb x y).

The command has indeed failed with message: Unable to satisfy the following constraints: In environment: A : Type x, y : A ?EqDec : "EqDec A"

制約を解消するために使われるアルゴリズムは eauto タクティックの類型で、それは補題 (インスタンス) の集合をもって証明探索を行います。それは typeclass_instances データベース内に定義された補題だけでなくローカルな仮定も使います。従ってこの例は以下のようにも書くことが出来ます:

Definition neqb' A (eqa : EqDec A) (x y : A) := negb (eqb x y).

neqb' is defined

しかしながら、替わりに型クラスの特別なサポートを持った束縛子の一般化を使うべきです:

• それらは型クラスの引数の状態を自動的に最大限暗黙に設定し、クラスメソッドのように簡単に使える派生関数を作ります。上の例では、A と eqa が最大限暗黙に設定されるはずです。

• それらは部分適用された型クラスの暗黙的な量化をサポートします (暗黙の一般化)。型クラスの束縛子の一部として与えられなかった引数も自動的に一般化されます。

• それらは スーパークラス に於ける暗黙の量化もサポートします。

以前の例に続き、次のように書くことが出来ます:

Generalizable Variables A B C.

Definition neqb_implicit `{eqa : EqDec A} (x y : A) := negb (eqb x y).

neqb_implicit is defined

ここでは A は暗黙的に一般化され、結果として得られる関数は上のそれに等しくなります。

パラメータ化されたインスタンス

インスタンスの前に束縛コンテキストとして制約を与えることで Haskell のようにパラメータ化されたインスタンスを簡潔に宣言することが出来ます。例えば:

Instance prod_eqb `(EA : EqDec A, EB : EqDec B) : EqDec (A * B) := { eqb x y := match x, y with              | (la, ra), (lb, rb) => andb (eqb la lb) (eqb ra rb)              end }.

1 subgoal A : Type EA : EqDec A B : Type EB : EqDec B ============================ forall x y : A * B, (let (la, ra) := x in let (lb, rb) := y in (eqb la lb && eqb ra rb)%bool) = true -> x = y

Abort.

これらのインスタンスは単にインスタンスヒントデータベースの中の補題として使われます。

セクションとコンテキスト

開発のパラメータ化を型クラスによって楽にするため、セクションの文脈に変数を導入する、暗黙引数の機構と互換な新しい方法を提供します。その新しいコマンドはどんな束縛コンテキストでも引数として受け入れるということを除き、Variables Vernacular と同じように動作します。例えば:

Section EqDec_defs.

Context `{EA : EqDec A}.

A is declared EA is declared

Global Instance option_eqb : EqDec (option A) :=   { eqb x y := match x, y with          | Some x, Some y => eqb x y          | None, None => true          | _, _ => false          end }.

1 subgoal A : Type EA : EqDec A ============================ forall x y : option A, match x with | Some x0 => match y with | Some y0 => eqb x0 y0 | None => false end | None => match y with | Some _ => false | None => true end end = true -> x = y

Admitted.

option_eqb is declared

End EqDec_defs.

About option_eqb.

option_eqb : forall A : Type, EqDec A -> EqDec (option A) Arguments A, EA are implicit and maximally inserted Argument scopes are [type_scope _] Expands to: Constant Top.option_eqb

ここで Global 修飾子はセクションの終わりでインスタンスを再宣言します。それはそれまで使うコンテキスト変数により一般化されていたものです。

階層の構築

スーパークラス

他のクラスによってクラスをパラメタライズし、クラスとスーパークラスの階層を生成することも出来ます。束縛コンテキストと同様に、スーパークラスを与えます:

Class Ord `(E : EqDec A) := { le : A -> A -> bool }.

Ord is defined le is defined

Haskell と違い、スーパークラスのために特別な構文はありませんが、この宣言は以下と等しくなります:

Class `(E : EqDec A) => Ord A :=
  { le : A -> A -> bool }.

この定義が意味するところは Ord クラスのインスタンスは EqDec のインスタンスを持っていなければならないということです。サブクラスのパラメータは少なくともそのスーパークラスのパラメータ全てをそれらの出現順で含みます (ここでは A ただ一つです)。これまで見てきたように、Ord は二つのパラメータ: A 型と EqDec A 型の E を持つレコードとして符号化されます。しかし、それでもそれを一般化束縛子の中で単一パラメータを持つかのように使うことができます: スーパークラスの一般化は自動的に行われます。

Definition le_eqb `{Ord A} (x y : A) := andb (le x y) (le y x).

le_eqb is defined

場合によっては、構造の共有を指定できるようにするため、スーパークラスを明示的に与えたいかもしれません。それは通常の束縛子の中では直接行い、そしてクラス束縛子の中では ! 修飾子を使うことで可能です。例えば:

Definition lt `{eqa : EqDec A, ! Ord eqa} (x y : A) := andb (le x y) (neqb x y).

lt is defined

この ! 修飾子は束縛子が解析される方法を切り替え、Coqの通常の解釈に戻します。特に、例で示したように、それは可能であれば暗黙引数の機構を使います。

部分構造

部分構造はクラスのインスタンス自身であるようなクラスの構成要素です。それらは論理的性質のためにクラスを使うときにたびたび現れます。例:

Require Import Relation_Definitions.

Class Reflexive (A : Type) (R : relation A) :=   reflexivity : forall x, R x x.

Class Transitive (A : Type) (R : relation A) :=   transitivity : forall x y z, R x y -> R y z -> R x z.

これは反射的および推移的関係のシングルトンクラスを宣言します (説明は singleton class 派生を見てください)。これらは他のクラスの一部として使うことが出来ます。

Class PreOrder (A : Type) (R : relation A) := { PreOrder_Reflexive :> Reflexive A R ;   PreOrder_Transitive :> Transitive A R }.

PreOrder is defined PreOrder_Reflexive is defined PreOrder_Transitive is defined

:> 構文は PreOrder それぞれが Reflexive 関係と見なせることを示しています。従って反射的関係が必要になるたび、代わりに前順序を使うことができます。これは Structure 定義のコアーション機構に非常に似ています。その実装は単純に各射影をインスタンスとして定義するものです。

同じ効果を達成するために Existing Instance コマンドを使うことで既存のオブジェクトや構造の射影を宣言することも出来ます。

コマンドの概要

Command Class ident binders? : sort? := ident? { ident :>? term+; }

Class コマンドはパラメータ binders とレコードフィールドを宣言するフィールドを伴う型クラスの宣言に使われます。

類型:

Command Class ident binders? : sort? := ident : term

この類型コマンドは単一のメソッドを持つ シングルトン クラスを定義します。このシングルトンクラスはいわゆる定義クラスといわれ、ident binders := term という定義として単純に表現され、そのインスタンスはこの型のオブジェクトそれ自体です。定義クラスはレコードの中に包まれておらず、そのようなクラスのインスタンスの自明な射影はそのインスタンスそれ自身と変換できます。これは簡単に既存のオブジェクトのインスタンスを作り、そして無駄な射影を挿入しないことで証明サイズを縮小するのに役立ちます。そのクラス定数自身は(訳注: 制約を)解消する間は固定的に指定され、そのためそのクラスの抽象は維持されます。

Command Existing Class ident

この派生形は定数や帰納的定義から事後的にクラスを宣言します。メソッドやインスタンスは定義されません。

Command Instance ident binders? : Class t1 … tn [| priority] := { field1 := b1 ; …; fieldi := bi }

Instance コマンドは ident という名前の型クラスインスタンスを宣言するのに使われます。クラス Class はパラメータ t1 から tn とフィールド b1 から bi を伴い、各フィールドはそのクラスの宣言されたフィールドでなければなりません。足りないフィールドは対話証明モードで埋められなければなりません。

パラメータ化されたインスタンスを宣言するためにインスタンスの名前の後かつコロンの前に binders の任意の文脈を置くことができます。任意に優先度を宣言することが出来、auto ヒントのためのもののように 0 が最高優先度です。優先度が指定されないならば、デフォルトはそのインスタンスの非依存束縛子の数になります。

Variant Instance ident binders? : forall binders?, Class t1 … tn [| priority] := term

この構文はシングルトンクラスインスタンスの宣言または forall binders, Class t1 … tn 型の明示的な項を直接与えるために使われます。シングルトンクラスについては一意なフィールド名に言及する必要すらありません。

Variant Global Instance

Global 修飾子はあるセクション中で宣言されたインスタンス上で、それらの一般化されたものがそのセクションが閉じられた後に自動的に再宣言されるように使うことができます。

Variant Program Instance

型検査を Program (章 Program) に切り替え、足りないフィールドを管理する(訳注: 証明)課題機構を使います。

Variant Declare Instance

このコマンドはあるモジュール型の中で、対応する具体的なインスタンスがこのモジュール型で何らかの実装として存在するべきだということを宣言します。これは Parameter と Definition または Declare Module と Module の差異に似ています。

Class と Instance Vernacular コマンドの他に、型クラスに関連するコマンドがいくつかあります。

Command Existing Instance ident+ [| priority]

このコマンドは、その型の最後に適用された型クラスが付くような定数の任意のリストを、任意に優先度を伴ってインスタンスデータベースへ追加します。それはセクションの終わりでインスタンスを再宣言したり、または構造の射影をインスタンスとして宣言するのに使えます。これは Print Instances のためにインスタンスを登録することを除いて Hint Resolve ident : typeclass_instances に相当します。

Command Context binders

与えられた束縛コンテキストに従って変数を宣言します。それは 暗黙の一般化 を使うかもしれません。

typeclasses eauto

このタクティックは eauto や auto と異なる(訳注: 制約)解消エンジンを使います。主な違いは以下です:

• eauto や auto とは異なり、(Coq 8.6 を基点として) 新しい証明エンジンの中で(訳注: 制約)解決全体が完了し、これは依存サブゴールの中でバックトラッキングが可能で、かつゴールの見送りがサポートされていることを意味します。typeclasses eauto はマルチゴールタクティックです。それは完全に独立したサブゴール上でのバックトラッキングを避けるため、サブゴール間の依存を解析します。

• 引数なしで呼ばれたときは、typeclasses eauto はデフォルトで (コアの替わりに) typeclass_instances データベースを使います。依存サブゴールは自動的に先送りにされ、先送りされたゴールは (Coq 8.5 の振る舞いに従い) 解消終了の後まで残ることがあります。

  注釈

  Coq 8.6 を基点として、 all:once (typeclasses eauto) は宣言されたクラスサブゴール だけ が型推論中に解消の開始と考えられる場合を除き、精細化/型推論の間にそれが呼ばれたとき型クラス解決の間に何が起きるかを忠実に模倣し、一方 all は非クラスサブゴールを選択できます。精細化エンジンがバックトラック出来るようになったとき、未来のバージョンではそれは all:typeclasses eauto に移行するかもしれません。

• 特定のデータベースを伴って呼ばれたとき (例. with) 、typeclasses eauto は先送りにされたゴールを検索中のどの時点でも残すことを許し、型クラスゴールを他と同じように扱います。

• データベースの透過性情報はそれらの中で定義された全てのヒントと一貫して使用されます。それは単一化器を呼ぶときに常に使われます。局所的な仮定を考えるとき、我々は与えられた最初のヒントデータベースの透過性状態を使います。展開可能変数と定数を伴う (例えば Create HintDb で作成された) 空のデータベースを typeclasses eauto の最初の引数として使うことにより、単一化の間局所的な仮定を使う(訳注: 制約の)解消に完全変換を使わせます。

Variant typeclasses eauto num

警告

num 制限の意味は auto と異なります。デフォルトでは、制限が与えられないならば検索は制限されません。auto と異なり、導入ステップは数えられ、その結果として auto より typeclasses eauto による検索の時はより大きい制限が必要とされるかもしれません。

Variant typeclasses eauto with ident+

この派生形は与えられたヒントデータベースでの解消を実行します。それは型クラスサブゴールを他のサブゴールと同じに扱います (特に非型クラスゴールに先送りがないときは)。

autoapply term with ident

タクティック autoapply はヒントデータベース ident の透過性情報を使用し term を適用し、型クラス解決は 行いません 。これは Hint Extern の中で (ヒントデータベース typeclass_instances の中の) 型クラスインスタンスのために、ヒントの適用時にローカルに型クラス解決を行うのではなく、補題の適用によって作られた型クラスサブゴール上でバックトラッキングを許すために使うことができます。

透明な型クラス、不透明な型クラス

Command Typeclasses Transparent ident+

このコマンドは型クラス解決の間識別子を透明にします。

Command Typeclasses Opaque ident+

型クラス検索のために識別子を不透明にします。ある定数がいくつかの単一化を阻み、(訳注: 型クラス)解決を失敗させる時に有益です。それは不動点や省略形のように見えない何かのような、証明探索中にけっして展開されるべきではない定数を宣言するのにも便利です。これはさらに、そのような固定的な定数によってインデックス出来る型クラスマップによって証明探索を高速化出来ます (see The hints databases for auto and eauto)。

デフォルトでは、全ての定数と局所変数は透明とみなされます。以下のような、型を省略するために使われる定数を不透明にしないように注意するべきです:

relation A := A -> A -> Prop.

これは Hint Transparent, Opaque ident : typeclass_instances に相当します。

Options

Flag Typeclasses Dependency Order

このオプション (8.6 からデフォルトで有効になった) はサブゴール間の依存順序を遵守し、その意味するところは、以前 (Coq 8.5 以下) では他のサブゴールが依存するサブゴールが優先され、一方非依存サブゴールは依存するもの前に置かれるということです。これは極めて異なった証明探索の性能挙動を示す可能性があります。

Flag Typeclasses Filtered Unification

このオプションは Coq 8.6 から使用可能でデフォルトで無効にされており、ヒント適用手続き filter-then-unify 戦略に切り替えます。ヒントを適用するため、まずそのゴールが推論やそのヒントによって指定されたパターンに構文的に マッチする かを検査し、そうなってはじめてそのヒントの結論とゴールを 単一化 しようと試みます。これは単一化を呼ぶ頻度が低くなることで劇的にパフォーマンスを改善でき、構文的パターンへのマッチングが非常に高速になります。これはインスタンスを持ち出すことに関して更なる制御性をも提供します。例えば、ある定数をパターン中に明示的に出現することを強制し、その場所にホールがあるゴール上でけっして適用させなくなります。

Flag Typeclasses Limit Intros

このオプション (デフォルトで有効) は生成された証明項の中で (関数的な) イータ展開を避けながらヒントを適用する能力を制御します。それはある積の中でマッチする積を伴うゴールに、イントロダクションを避けて直接積を適用して結論を出すヒントを認めることで行います。

警告

これはヒント節の動的な再構築を要求するため高くつく可能性があります、そして積の導入規則の反転可能性から恩恵を得られず、結果として証明探索がより高価になる (つまり、よりバックトラッキングが役に立たなくなる) 可能性があります 。

Flag Typeclass Resolution For Conversion

このオプション (デフォルトで有効) は精緻化/型推論の間に単一化問題が解決できない時に型クラス解決の使用を制御します。このオプションが有効なことにより、単一化が失敗したとき、再度単一化を起動する前に型クラス解決が試行されます。

Flag Typeclasses Strict Resolution

このオプションが設定されたときに導入された型クラス宣言はより厳密な解決時の振る舞いを持ちます。(このオプションはデフォルトで無効です)このクラスのインスタンスによりゴールの単一化を求めている時、そのゴールに現れる全ての存在量化された変数を "凍結" します。これは単一化の間固定され、インスタンス化できないと見なされることを意味しています。

Flag Typeclasses Unique Solutions

型クラス解決が起きた時、それが単一の解を持たないならば失敗することを保証します。これはその解が正準であることを保証しますが、証明探索はより高価になりえます。

Flag Typeclasses Unique Instances

このオプションが設定された時に導入された型クラス宣言は、より効率的な解決時の振る舞いを持っています。(このオプションはデフォルトで無効です)。このクラスの型クラスゴールの解が見つかったとき、けっしてバックトラックを行わず、それが正準であると仮定します。

Flag Typeclasses Debug

型クラス解決のステップが検索中に表示されるかどうかを制御します。またこのフラグは Typeclasses Debug Verbosity を 1 に設定します。

Option Typeclasses Debug Verbosity num

どれくらいの情報が型クラス解決のステップが検索中に表示されるかを決定します。1 はデフォルトレベルです。2 は追加の情報を表示します。例えばタクティックやゴールの先送りなどです。このオプションを設定すると Typeclasses Debug も設定します。

Flag Refine Instance Mode

このオプションは Instance コマンドを通じて行われるインスタンス宣言の振る舞いの切り替えを認めます。

• それが有効 (デフォルト) なとき、証明項に未解決のホールを持つインスタンスは、残っている証明すべき課題を伴って無言で証明モードを開きます。

• 無効なときは、替わりにエラーを伴って失敗します。

型クラスの eauto :=

Command Typeclasses eauto := debug? {dfs | bfs}? depth

このコマンドは型クラス解決タクティックのより広範囲のカスタマイズを行います。オプションの意味は:

• debug デバッグモードでは、成功裏に適用されたタクティックのトレースが表示されます。

• dfs, bfs これは検索戦略を深さ優先探索 (デフォルト) または幅優先探索に設定します。

• depth これはその検索の深さ制限を設定します。