Skip to content

Commit

Permalink
[ fix ] eta-expand tests
Browse files Browse the repository at this point in the history
  • Loading branch information
gallais committed Mar 26, 2024
1 parent 116327d commit 337d44c
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 2 deletions.
2 changes: 1 addition & 1 deletion tests/prelude/char001/chars.idr
Original file line number Diff line number Diff line change
@@ -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
Expand Down
2 changes: 1 addition & 1 deletion tests/prelude/nat001/nats.idr
Original file line number Diff line number Diff line change
@@ -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
Expand Down

0 comments on commit 337d44c

Please sign in to comment.