diff --git a/libs/prelude/Prelude/Basics.idr b/libs/prelude/Prelude/Basics.idr index dc5be05612..d275c2c0b5 100644 --- a/libs/prelude/Prelude/Basics.idr +++ b/libs/prelude/Prelude/Basics.idr @@ -22,7 +22,7 @@ Not x = x -> Void ||| @ a the type to assign ||| @ x the element to get the type public export %inline -the : (0 a : Type) -> (x : a) -> a +the : (0 a : Type) -> (1 x : a) -> a the _ x = x ||| Identity function. diff --git a/tests/prelude/char001/chars.idr b/tests/prelude/char001/chars.idr index 0b9a4fe0c9..e7219d53fc 100644 --- a/tests/prelude/char001/chars.idr +++ b/tests/prelude/char001/chars.idr @@ -1,5 +1,5 @@ chars : List Char -> List Char -chars = the (List Char) +chars cs = the (List Char) cs singletonRange : chars ['1'..'1'] = chars ['1'] singletonRange = Refl diff --git a/tests/prelude/nat001/nats.idr b/tests/prelude/nat001/nats.idr index 3979b3e526..15b97d362e 100644 --- a/tests/prelude/nat001/nats.idr +++ b/tests/prelude/nat001/nats.idr @@ -1,5 +1,5 @@ nats : List Nat -> List Nat -nats = the (List Nat) +nats ns = the (List Nat) ns singletonRange : nats [1..1] = nats [1] singletonRange = Refl