intellij-arend
intellij-arend copied to clipboard
Warning when attempting to patternmatch on unimported constructors
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
}