From 337d44c8b5e435244464a38733f646b33e1f7309 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Tue, 26 Mar 2024 14:57:07 +0000 Subject: [PATCH] [ fix ] eta-expand tests --- tests/prelude/char001/chars.idr | 2 +- tests/prelude/nat001/nats.idr | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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