We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
44c2d16
Alow absurd patterns, e.g.
fun nomatchTest (n : N) (_: Id (succ (succ n)) (succ n)) : N where | n k !@ k