小编m0d*_*vis的帖子

我很容易获得一个Keys列表,如下所示:

open import Relation.Binary
open import Relation.Binary.PropositionalEquality using (_?_)

module AVL-Tree-Functions
  { k v ? } { Key : Set k }
  ( Value : Key ? Set v )
  { _<_ : Rel Key ? }
  ( isStrictTotalOrder : IsStrictTotalOrder _?_ _<_ )
  where

  open import Data.AVL Value isStrictTotalOrder public

  open import Data.List.Base
  open import Function
  open import Data.Product

  keys : Tree ? List Key
  keys = Data.List.Base.map proj? ? toList

但我不清楚如何指定返回值列表的函数类型.这是我的第一次尝试:

  -- this fails to typecheck
  values : …

不小心,我设法让实例搜索成功,但我不明白为什么.

在下面的代码中,为什么test2成功但test1失败(有未解决的元数据和约束)？如何添加? isRelation ?参数来IsSymmetric2帮助？我认为它必须以某种方式与一些metas得到解决,因此允许实例搜索成功,但除此之外,我很有雾.

有人能否说明这里的工作机制？

有一个答案在这里触及我的问题(以下简称"弱点"一节)上,但没有解释出现的解决方法是如何工作的力学.我猜这个问题的答案将帮助我更好地理解这种解决方法.

{-# OPTIONS --show-implicit #-}

record IsSymmetric1 {A : Set} (F : A ? A ? A) (Q : A ? A ? Set) : Set where
  field
    symmetry1 : ? {x y} ? Q (F x y) (F y x)

open IsSymmetric1 ? … ?

record IsRelation {A : Set} (Q : A ? A ? Set) : Set where
  no-eta-equality

record IsSymmetric2 {A …