summaryrefslogtreecommitdiff
path: root/src/data/lib/prim/Agda/Builtin/List.agda
diff options
context:
space:
mode:
Diffstat (limited to 'src/data/lib/prim/Agda/Builtin/List.agda')
-rw-r--r--src/data/lib/prim/Agda/Builtin/List.agda7
1 files changed, 6 insertions, 1 deletions
diff --git a/src/data/lib/prim/Agda/Builtin/List.agda b/src/data/lib/prim/Agda/Builtin/List.agda
index 98958ab..d5d5946 100644
--- a/src/data/lib/prim/Agda/Builtin/List.agda
+++ b/src/data/lib/prim/Agda/Builtin/List.agda
@@ -1,3 +1,4 @@
+{-# OPTIONS --without-K #-}
module Agda.Builtin.List where
@@ -14,4 +15,8 @@ data List {a} (A : Set a) : Set a where
{-# COMPILED_DATA List MAlonzo.Code.Agda.Builtin.List.AgdaList [] (:) #-}
{-# COMPILED_DATA_UHC List __LIST__ __NIL__ __CONS__ #-}
-
+{-# COMPILED_JS List function(x,v) {
+ if (x.length < 1) { return v["[]"](); } else { return v["_∷_"](x[0], x.slice(1)); }
+} #-}
+{-# COMPILED_JS [] Array() #-}
+{-# COMPILED_JS _∷_ function (x) { return function(y) { return Array(x).concat(y); }; } #-}