module Juvix.Builtin.V1.List;

import Juvix.Builtin.V1.Fixity open;

syntax operator List.:: cons;

--- Inductive list.
builtin list
type List (A : Type) :=
  | --- The empty list
    nil
  | --- An element followed by a list
    :: A (List A);

open List using {nil; ::} public;