val last: l:list 'a {Cons? l} -> Tot 'a
let rec last = function
  | [hd] -> hd
  | _::tl -> last tl
val last: l:list 'a {Cons? l} -> Tot 'a
let rec last =
function
| [hd] -> hd
| _ :: tl -> last tl
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.b2t Prims.uu___is_Cons FStar.List.Tot.Base.last
(*
   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
l: Prims.list 'a {Cons? l} -> 'a