    {-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness --level-universe #-}

    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); }; } #-}