intellij-arend icon indicating copy to clipboard operation
intellij-arend copied to clipboard

Warning when attempting to patternmatch on unimported constructors

Open sxhya opened this issue 1 year ago • 0 comments

In this code sample true and false should be highlighted as variables, whose names clash with the names of the (unimported) constructors of the datatype Bool.

\import Data.Bool(Bool, if)

\func bar (b : Bool) : Nat => \case b \with {
  | true => 1
  | false => 0
} 

sxhya avatar Mar 06 '23 17:03 sxhya