小编pro*_*ver的帖子

我正在尝试编写一个形式为f : (X + Y) -> (Z + T)where X, Y, Z, Tare types的函数，它+是 sum 类型的伪符号。的返回类型f将由上下文确定，即在伪 agda 中

postulate x : X

t : T
t = f x -- OK, since (f : X -> T) definition is used

制作这样的东西很容易（再次在伪 agda 中，我试图简洁明了）：

fromX : X -> X + Y
toT : Z x T -> T

t2 : T
t2 = toT (f (fromX x))

但这对于我想要完成的事情来说太吵了。我尝试滥用实例查找。这是我想要工作但不进行类型检查的最小代码：

module Agda2 where
  infix 21 _·_ …