parsing - 基于 Agda 上的一篇论文在 Idris 中实现 Total Parser

Answer 1

目前正在尝试自己移植这个库，似乎 Agda 向 Idris 推断出不同的隐含。这些是缺少的隐式：

%default total

mutual
  data P : Bool -> Type where
    Fail : P False
    Empty : P True
    Tok : Char -> P False
    (<|>) : P n -> P m -> P (n || m)
    (.) : {n,m: Bool} -> LazyP m n -> LazyP n m -> P (n && m)

  LazyP : Bool -> Bool -> Type
  LazyP False n = Inf (P n)
  LazyP True  n = P n

lr : P False
lr = (.) {n=False} {m=False} (Delay lr) (Delay lr)