[ prelude ] the is linear in its input (#3239)

* [ prelude ] `the` is linear in its input * [ fix ] eta-expand tests
idris-lang · Mar 27, 2024 · 2c2aa85 · 2c2aa85
1 parent 1c186f0
commit 2c2aa85
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git 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
@@ -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
@@ -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