HdTl.v 512 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below    *)
Require Import BuiltIn.
Require BuiltIn.
Require list.List.
Require option.Option.

(* Why3 assumption *)
Definition hd {a:Type} {a_WT:WhyType a} (l:(list a)): (option a) :=
  match l with
  | nil => None
  | (cons h _) => (Some h)
  end.

(* Why3 assumption *)
Definition tl {a:Type} {a_WT:WhyType a} (l:(list a)): (option (list a)) :=
  match l with
  | nil => None
  | (cons _ t) => (Some t)
  end.