diff --git a/drivers/ocaml.drv b/drivers/ocaml.drv index 126a04ad0cfd92875cb8d7cd57cc66c1263940d8..37d2a5e0a456c258ee4025719900d04be913e7f4 100644 --- a/drivers/ocaml.drv +++ b/drivers/ocaml.drv @@ -38,6 +38,19 @@ theory list.List syntax function Cons "((%1) :: (%2))" end +theory list.Length + syntax function length "(List.length (%1))" +end + +theory list.Append + syntax function (++) "(List.append (%1) (%2))" +end + +theory list.Reverse + syntax function reverse "(List.rev (%1))" +end + + (* WhyML *) diff --git a/theories/list.why b/theories/list.why index 5a8c72dd6d8fa3916e64ddd031b8a4c1bc1fcc9d..afebed0c5809957855f1e6ec0f777dcbbd2602d8 100644 --- a/theories/list.why +++ b/theories/list.why @@ -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 end +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 + +end + (** {2 Relation between head, tail, and nth} *) theory NthHdTl