Agda-2.3.2.2: test/fail/AbsurdPatternRequiresNoRHS.agda

module AbsurdPatternRequiresNoRHS where

data   False : Set where
record True  : Set where

f : False -> True
f () = _