在 Idris2 中，无法键入检查是否直接

Question

我是Idris的初学者。在Idris2 0.3.0版本中，我观察到了一个奇怪的行为。

为什么这个代码类型不检查？

f : Type -> Type -> Type
f a b = (c : Bool) -> if c then a else b

While processing right hand side of f. Main.case block in f is not accessible in this context.

而这种代码类型检查没有问题：

f1 : Type -> Type -> Bool -> Type
f1 a b c = if c then a else b
f' : Type -> Type -> Type
f' a b = (c : Bool) -> f1 a b c

这是个虫子吗？

起初，我试图证明一个愚蠢的定理，这个定理应该是显而易见的，但Refl不起作用。看起来它无法理解变量是否匹配。

module Main
import Data.Nat
t : Nat -> Nat -> Nat
t l r = if lte l r then l else r
prop : Nat -> Nat -> Type
prop a b = (t a b = if lte a b then a else b)
proof_prop : prop a b
proof_prop = ?imlost

Answer 1

您的if_then_else_使用程序在提交04a0f5001f:时开始失败

检查Pi绑定时更正乘法

我们一直只使用0，如果函数正在运行，这是不正确的以便在运行时模式匹配中使用。现在正确计算，以便我们明确了在运行时使用哪些类型级别的变量。

如果使用计算Pi类型的函数。解决方案是函数显式为0重数。如果不起作用，你可以在运行时意外尝试使用仅编译时数据时间

修复#1163

解决方案是将f函数标记为仅类型级别：

0 f : Type -> Type -> Type
f a b = (c : Bool) -> if c then a else b