Agda中的类型类的实例）
Agda的记录组合和instance关键字使我们的行为与Haskell的类型类相似。 此外，忽略instance关键字，我们可以为同一类型提供多个实例 - 这是我们在Haskell中无法做到的。
我处于一个需要Haskell一个实例的要求，但在Agda。 有没有编译器选项或一些技巧/启发式强制执行此？
现在我采取的方法是，
record Yo (n : ℕ) : Set where
field
sem : (some interesting property involving n)
open Yo {{...}}
postulate UniqueYo: ∀ {n} (p q : Yo n) → p ≡ q
然而，每当我真正使用UniqueYo ，缺乏计算就会让我的目标散布诸如...| UniqueYo pp东西 ...| UniqueYo pp ，我更喜欢...| refl ...| refl或全部重写到正常形式代替。
任何帮助表示赞赏！
链接地址: http://www.djcxy.com/p/33171.html