Instantly share code, notes, and snippets.

@ziman /dot.idr
Created Apr 11, 2014

Embed
What would you like to do?
Dot avoidance
data T : Nat -> Type where
C : .(n : Nat) -> T n
f : (n : Nat) -> T n -> Bool
f Z (C Z ) = True
f (S n) (C (S n)) = f n (C n)
main : IO ()
main = print $ f 3 (C 3)
{-
Main.C: inaccessible arguments reachable:
n from Main.f arg# 1
Main.f {e0} {e1} =
case {e1} of
| 0 => Prelude.Bool.True
| _ => let {e3} = LMinus (ATInt ITBig)({e1}, 1) in Main.f(____, {e3})
-}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment