No warning about useless `{-# CATCHALL #-}` pragma

agda / agda

Agda is a dependently typed programming language / interactive theorem prover.

https://wiki.portal.chalmers.se/agda/pmwiki.php

Other

2.41k stars 339 forks source link

No warning about useless `{-# CATCHALL #-}` pragma #7321

Open andreasabel opened 1 week ago

andreasabel commented 1 week ago

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