parsing - Agda に関する論文に基づく Idris でのトータル パーサーの実装

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)