{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness
--no-subtyping #-}
module Agda.Builtin.List where
infixr 5 _∷_
data List {a} (A : Set a) : Set a where
[] : List A
_∷_ : (x : A) (xs : List A) → List A
{-# BUILTIN LIST List #-}
{-# COMPILE JS List = function(x,v) {
if (x.length < 1) { return v["[]"](); } else { return v["_∷_"](x[0], x.slice(1)); }
} #-}
{-# COMPILE JS [] = Array() #-}
{-# COMPILE JS _∷_ = function (x) { return function(y) { return Array(x).concat(y); }; } #-}