val append: list 'a -> list 'a -> Tot (list 'a)
let rec append x y = match x with
  | [] -> y
  | a::tl -> a::append tl y
val append: list 'a -> list 'a -> Tot (list 'a)
let rec append x y =
match x with
| [] -> y
| a :: tl -> a :: append tl y
FStar.List.Tot.Base.fst.checked
prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked
FStar.List.Tot.Base.fst
Prims.list Prims.Cons FStar.List.Tot.Base.append
(*
   Copyright 2008-2014 Nikhil Swamy and Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
(**
This module defines all pure and total operations on lists that can be
used in specifications. It is implemented by FStar_List_Tot_Base.ml, any
functional change and/or the addition of new functions MUST be reflected
there.

@summary Pure total operations on lists
*)
module FStar.List.Tot.Base

(**
Base operations
*)

(** [isEmpty l] returns [true] if and only if [l] is empty  *)
val isEmpty: list 'a -> Tot bool
let isEmpty l = match l with
  | [] -> true
  | _ -> false

(** [hd l] returns the first element of [l]. Requires [l] to be
nonempty, at type-checking time. Named as in: OCaml, F#, Coq *)
val hd: l:list 'a{Cons? l} -> Tot 'a
let hd = function
  | hd::_ -> hd

(** [tail l] returns [l] without its first element. Requires, at
type-checking time, that [l] be nonempty. Similar to: tl in OCaml, F#, Coq
*)
val tail: l:list 'a {Cons? l} -> Tot (list 'a)
let tail = function
  | _::tl -> tl

(** [tl l] returns [l] without its first element. Requires, at
type-checking time, that [l] be nonempty. Named as in: OCaml, F#, Coq
*)
val tl: l:list 'a {Cons? l} -> Tot (list 'a)
let tl = tail

(** [last l] returns the last element of [l]. Requires, at
type-checking time, that [l] be nonempty. Named as in: Haskell
*)
val last: l:list 'a {Cons? l} -> Tot 'a
let rec last = function
  | [hd] -> hd
  | _::tl -> last tl

(** [init l] returns [l] without its last element. Requires, at
type-checking time, that [l] be nonempty. Named as in: Haskell
*)
val init: l:list 'a {Cons? l} -> Tot (list 'a)
let rec init = function
  | [_] -> []
  | hd::tl -> hd::(init tl)

(** [length l] returns the total number of elements in [l]. Named as
in: OCaml, F#, Coq *)
val length: list 'a -> Tot nat
let rec length = function
  | [] -> 0
  | _::tl -> 1 + length tl

(** [nth l n] returns the [n]-th element in list [l] (with the first
element being the 0-th) if [l] is long enough, or [None]
otherwise. Named as in: OCaml, F#, Coq *)
val nth: list 'a -> nat -> Tot (option 'a)
let rec nth l n = match l with
  | []     -> None
  | hd::tl -> if n = 0 then Some hd else nth tl (n - 1)

(** [index l n] returns the [n]-th element in list [l] (with the first
element being the 0-th). Requires, at type-checking time, that [l] be
of length at least [n+1]. *)
val index: #a:Type -> l:list a -> i:nat{i < length l} -> Tot a
let rec index #a (l: list a) (i:nat{i < length l}): Tot a =
  if i = 0 then
    hd l
  else
    index (tl l) (i - 1)

(** [count x l] returns the number of occurrences of [x] in
[l]. Requires, at type-checking time, the type of [a] to have equality
defined. Similar to: [List.count_occ] in Coq. *)
val count: #a:eqtype -> a -> list a -> Tot nat
let rec count #a x = function
  | [] -> 0
  | hd::tl -> if x=hd then 1 + count x tl else count x tl

(** [rev_acc l1 l2] appends the elements of [l1] to the beginning of
[l2], in reverse order. It is equivalent to [append (rev l1) l2], but
is tail-recursive. Similar to: [List.rev_append] in OCaml, Coq. *)
val rev_acc: list 'a -> list 'a -> Tot (list 'a)
let rec rev_acc l acc = match l with
    | [] -> acc
    | hd::tl -> rev_acc tl (hd::acc)

(** [rev l] returns the list [l] in reverse order. Named as in: OCaml,
F#, Coq. *)
val rev: list 'a -> Tot (list 'a)
let rev l = rev_acc l []

(** [append l1 l2] appends the elements of [l2] to the end of [l1]. Named as: OCaml, F#. Similar to: [List.app] in Coq. *)
val append: list 'a -> list 'a -> Tot (list 'a)
x: Prims.list 'a -> y: Prims.list 'a -> Prims.list 'a