This passes without warning:
open import Agda.Builtin.Nat
open import Agda.Builtin.Bool
isZero : Nat → Bool
isZero 0 = true
{-# CATCHALL #-} -- This pragma is useless!
isZero (suc n) = false
Would be nice to get a warning and some deadcode highlighting for the pragma.
CC: @jespercockx
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4