Agda considers catchall clauses that omit the matched arguments on the LHS as exact, for example the last clause here isn't highlighted and doesn't throw a warning:
{-# OPTIONS --exact-split #-}
open import Agda.Builtin.Bool
not : Bool → Bool
not false = true
not = λ _ → false
This also causes the following non-terminating function to be accepted, because the termination checker uses exact clauses to reduce away function calls (see #5065):
open import Agda.Builtin.Bool bad : Bool → Bool bad true = bad true bad = λ _ → true
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