From 881902f2c7b4a690dd512b750cbc82f2d954f1e9 Mon Sep 17 00:00:00 2001 From: artoy Date: Thu, 24 Aug 2023 23:58:42 +0900 Subject: [PATCH] update tests --- src/test/list/nth.imp | 21 +++++++++++++++++++-- 1 file changed, 19 insertions(+), 2 deletions(-) diff --git a/src/test/list/nth.imp b/src/test/list/nth.imp index 59dbff12..6ba96e1e 100644 --- a/src/test/list/nth.imp +++ b/src/test/list/nth.imp @@ -1,7 +1,24 @@ -nth(l, n) { +mklist(n) { + if n = 0 then Nil else { + let h = _ in + let m = n + -1 in + let t = mkref mklist(m) in + Cons h t + } +} +nth(l, n) { + match l with + Nil -> fail + | Cons h t -> { + let m = n + -1 in + if n = 1 then h else nth(*t, m) + } } { - + let n = ( _ : ~ >= 1) in + let k = ( _ : ~ >= 1 /\ ~ <= n) in + let l = mklist(n) in + nth(l, k) } \ No newline at end of file