JetBrains / intellij-arend

Arend plugin for IntelliJ IDEA
Apache License 2.0
90 stars 12 forks source link

False positive redundant parentheses inspection #550

Closed sxhya closed 2 months ago

sxhya commented 2 months ago
\func ::-++ {X : \Type} {x : X} {xs y : List X} : (x :: xs) ++ y = x :: (xs ++ y) \elim xs
  | nil => idp
  | a :: y => idp

\func foo (x : Nat) (p : Bool) (a : \Sigma Nat Bool) (u1 u2 : List (\Sigma Nat Bool)) => 
   ::-++ {_} {a} {u1} {(x, p) :: (x, not p) :: u2} -- false positive 'Redundant parentheses' reported on (x, p)