good first issue
描述
{-@ inline id' @-}
id' x = x
{-@ arith :: { id' ( 2 <= 2 ) } @-}
arith = ()
yields:
/home/zgrannan/rewriting-paper/optimization/arith.hs:4:20: error: Cannot parse specification:
unexpected "( "
expecting "&&", "->", "<:", "<=>", "==>", "=>", "||", "~>", ':', '}', or monoPredicateP
This is a contrived example but I've run into similar issues generating LH specifications programmatically.
In general I would expect that if the expression {-@ thm : { x } @-} parses, then {-@ thm : { id' (x) } @-} should also parse (excluding the LH builtin operators not already present in Haskell, such as <=>)