Commit cfdcbe98 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

tests in examples/list.why

parent 933df2e7
theory Induction2
use import list.List
use import list.Length
logic p ('a list, 'b list)
axiom Induction :
p(Nil : 'a list, Nil : 'b list) ->
(forall x1:'a, x2:'b, l1:'a list, l2:'b list.
p(l1, l2) -> p(Cons(x1,l1), Cons(x2,l2))) ->
forall l1:'a list, l2:'b list. length(l1)=length(l2) -> p(l1, l2)
end
theory Test1
use export int.Int
use export list.List
use export list.Length
goal G1 : length(Cons(1, Nil)) = 1
goal G2 : length(Cons(1, Cons (2, Nil))) = 1 + 1
logic zip(l1 : 'a list, l2 : 'b list) : ('a * 'b) list =
match l1, l2 with
| Cons (x1, r1), Cons (x2, r2) -> Cons ((x1, x2), zip (r1, r2))
| _, _ -> Nil (* to make it total *)
end
logic foo(l1 : 'a list, l2 : 'b list) =
length(zip(l1, l2)) = length(l1)
clone Induction2 with logic p = foo
goal G3 : forall l1: 'a list, l2 : 'b list.
length(l1) = length(l2) ->
length(zip(l1, l2)) = length(l1)
goal G4 : zip(Cons(1, Cons(2, Nil)),
Cons(1., Cons(2., Nil))) =
Cons ((1, 1.), Cons((2, 2.), Nil))
end
......@@ -427,9 +427,9 @@ let do_input env drv = function
Queue.iter (do_local_theory drv fname m) tlist
with
| Loc.Located (loc, e) ->
eprintf "%a%a" Loc.report_position loc report e; exit 1
eprintf "%a%a@." Loc.report_position loc report e; exit 1
| e ->
report err_formatter e; exit 1
eprintf "%a@." report e; exit 1
let () =
try
......
......@@ -15,7 +15,7 @@ theory Int
clone export relations.TotalOrder with
type t = int, logic rel = (<=)
end
end
theory Abs
......
Supports Markdown
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