Commit 56cfc3d2 authored by MARCHE Claude's avatar MARCHE Claude

Extraction of List. append, reverse, length

new theory HdTlNoOpt
parent 45fa2f33
......@@ -38,6 +38,19 @@ theory list.List
syntax function Cons "((%1) :: (%2))"
theory list.Length
syntax function length "(List.length (%1))"
theory list.Append
syntax function (++) "(List.append (%1) (%2))"
theory list.Reverse
syntax function reverse "(List.rev (%1))"
(* WhyML *)
......@@ -77,7 +77,7 @@ theory NthNoOpt
use export List
use import int.Int
function nth (n: int) (l: list 'a) : 'a
function nth (n: int) (l: list 'a) : 'a
axiom nth_cons_0: forall x:'a, r:list 'a. nth 0 (Cons x r) = x
axiom nth_cons_n: forall x:'a, r:list 'a, n:int.
......@@ -121,6 +121,20 @@ theory HdTl
theory HdTlNoOpt
use export List
function hd (l: list 'a) : 'a
axiom hd_cons: forall x:'a, r:list 'a. hd (Cons x r) = x
function tl (l: list 'a) : list 'a
axiom tl_cons: forall x:'a, r:list 'a. tl (Cons x r) = r
(** {2 Relation between head, tail, and nth} *)
theory NthHdTl
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment