greatBigDot

Results 2 issues of greatBigDot

Using double quotes ('"') or character sequences for comments ("--" or "{-") in inline documentation severely messes up the highlighting.

2 comment

I ran into some odd behavior when using Idris' inline documentation features. I first noticed the problem when using double quotes: ||| This is a representation of a "Magma", an...

Singletonize functions that already use singletons

1 comment

$(singletons [d| data Nat = Z | S Nat data Vec n a where VNil :: Vec 'Z a (:::) :: a -> Vec n a -> Vec ('S n)...

enhancement