summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
authorAlexey Radul <axch@google.com>2023-04-04 15:56:19 -0400
committeraxch <233710+axch@users.noreply.github.com>2023-04-05 11:10:16 -0400
commit1ae0689f0015ffe37c3fdd361baa7f4193f6796f (patch)
tree162657470aa18d4925dd0b52ed64383449d71626 /tests
parent5edfffe7a7a771030efab2287cb53e74eac24d1c (diff)
An explicit test that we have a syntax for writing lambdas that take implicit arguments.
Diffstat (limited to 'tests')
-rw-r--r--tests/typeclass-tests.dx6
1 files changed, 6 insertions, 0 deletions
diff --git a/tests/typeclass-tests.dx b/tests/typeclass-tests.dx
index e48e373b..2e290b60 100644
--- a/tests/typeclass-tests.dx
+++ b/tests/typeclass-tests.dx
@@ -221,3 +221,9 @@ data_id [4, 5, 6]
data_id (the (n:Nat &> (Fin n) => Nat) (3 ,> [5, 6, 7]))
> (3 ,> [5, 6, 7])
+
+----------------- Lambda function taking class arguments -----------------
+
+:t \(given (a|Ix, b|Ix) (Subset a b)) (xs:a=>Float). xs[0@_]
+> ({a:Type}[d:(Ix a)]{b:Type}[d.1:(Ix b),v#0:(Subset a b)](xs:(a
+> => Float32)) -> Float32)