Dafny でポリモーフィック バイナリ リレーション タイプ (クラス) を定義しました。
class binRel<S,T>
実際の宣言は次のとおりです。
class binRel<S(!new,==),T(!new,==)>.
新しい型制約を追加したいと思います。型 S と T は "表示" 操作 (文字列を返す) を実装する必要があります。
私が Dafny リファレンス マニュアルを読んだところ、Dafny がサポートする組み込みの型制約は == と明らかに !new のみであり、特定のトレイトなど、その型のサポートを要求する方法はありません。
おそらく私は間違っており、リファレンス マニュアルよりも最近の更新でそのような機能が提供されています。私は運がいいですか？そうでない場合、おそらく回避策はありますか？