是否导入了％提示注释/ Dec和自动注释？

Question

我有一个依赖于谓词P：a - > Type的数据类型，这意味着它的一些数据构造函数引用具有隐式P x作为参数。我想idris能够自动推断这种隐含。为此，我用关键字auto注释了隐式，我在类型声明之前写了一个函数isP：（x：a） - > Dec（P x），带有％hint注释。即，像：

module P

P : a -> Type

%hint
isP : (x : a) -> Dec (P x)

并在一个单独的文件中

module Main

import P

data Foo : Type where
  Bar : (x : a) -> .{auto prf : P x} -> Foo

也就是说，我无法声明所述Foo类型的值，因为Idris声称它无法推断出prf。

这是因为prf的类型是P x而不是Dec（P x），还是因为％hint标志没有导入？

在任何一种情况下，我如何让Idris使用Dec值来尝试找到隐含的？

Answer 1

正如你所猜想的那样导入%hint标志，因为Dec (P x)与P x不同。

但是有一个技巧，你可以使用这个数据类型：

data IsYes : prop -> Type where
  SoTrue : IsYes (Yes prop)

（基本上，你定义了一个包含给定属性的Yes的类型）然后你可以使用default而不是auto来检查属性是否成立：

data Foo : Type where
  Bar : (x : a) -> .{default SoTrue prf : IsYes (isP x)} -> Foo

注意：有了这个技巧，你甚至不再需要%hint了，你只需要在编译时检查isP的结果。