我想在Idris中编写一条记录，但它有一个通用参数，需要受到接口的约束。对于正常的联盟类型，我可以这样写： data BSTree : (a : Type) -> Type where
Empty : Ord a => BSTree a
Node : Ord a => BSTree a -> a -> BSTree a
但我试图找出做同样的事情，只是用记录的语法。我试过类似
由于类型是伊德里斯一流的，好像我应该能够编写一个typeOf函数返回其参数的类型： typeOf : a => a -> Type
typeOf x = a
然而，当我试图调用这个函数，我得到看起来像一个错误： *example> typeOf 42
Can't find implementation for Integer
我怎样才能正确地实现这个功能typeOf？或者是否存在一些我
我写这个函数： ||| Returns the ten largest values in the list.
top_ten : Ord a => List a -> List a
我第一次尝试是一个pointfree实现使用功能组成： top_ten = take 10 . reverse . sort
但是这给了以下错误： Main.idr:3:9:When checking ri
IO`操作考虑： *lecture2> :let x = (the (IO Int) (pure 42))
看着它的类型，有什么MkFFI C_Types String String签名的含义是什么？ *lecture2> :t x
x : IO' (MkFFI C_Types String String) Int
然后我尝试从REPL评估x： *lecture2> :exec x
m
我正在与Idris语法打交道，看来。 module Test
data Nat = Z | S Nat
Eq Nat where
Z == Z = True
S n1 == S n2 = n1 == n2
_ == _ = False
这抱怨，出现以下错误（V1.1.1）： .\.\Test.idr:5:8: error: expected: "@",