Idris2/tests/idris2/reg041/tuple.idr

mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-13 17:25:29 +03:00
tupleBug : Pair () a -> ()
tupleBug (_, _, _) = ()

odd : a -> Bool
odd () = False
Only fully normalise fromInteger on LHS This reduces surprising undefined name errors on the RHS, as noted in issue #1541 2021-06-12 16:23:25 +03:00			`tupleBug : Pair () a -> ()`
			`tupleBug (_, _, _) = ()`

			`odd : a -> Bool`
			`odd () = False`