prelude

parent 5484f326
theory Array
type ('a,'b) t
theory IntArray
logic select (('a,'b) t,'a) : 'b
logic store (('a,'b) t,'a,'b) : ('a,'b) t
axiom select_eq : forall m : ('a,'b) t. forall a1,a2 : 'a. forall b : 'b.
a1=a2 -> Eq.eq(select(store(m,a1,b),a2),b)
axiom select_eq : forall m : ('a,'b) t. forall a1,a2 : 'a. forall b : 'b.
not a1 = a2 -> select(store(m,a1,b),a2) = select(m,a2)
logic const ('b) : ('a,'b) t
axiom const : forall b:'b. forall a:'a. select(const(b),a) = b
use import prelude.Int
use import prelude.Array
end
(*
Local Variables:
compile-command: "make -C ../.. test"
End:
*)
type t = | True | False
\ No newline at end of file
......@@ -3,7 +3,23 @@
theory IntList
use prelude.List
use import prelude.Int
use import prelude.List
logic sorted(int list)
axiom Sorted_nil :
sorted(nil)
axiom Sorted_one :
forall x: int. sorted(cons(x, nil))
axiom Sorted_cons:
forall x,y: int. forall l: int list.
sorted(cons(y, l)) -> le(x, y) -> sorted(cons(x, cons(y, l)))
end
(*
Local Variables:
compile-command: "make -C ../.. test"
End:
*)
......@@ -5,6 +5,17 @@ theory Int
type int
logic lt(int, int)
logic le(int, int)
logic gt(int, int)
logic ge(int, int)
end
theory Bool
(*type t = | True | False*)
end
theory List
......@@ -49,3 +60,9 @@ theory Array
axiom Const : forall b:'b. forall a:'a. Eq.eq(select(const(b),a), b)
end
(*
Local Variables:
compile-command: "make -C ../.. test"
End:
*)
......@@ -4,6 +4,7 @@
theory TestPrelude
use prelude.List
use list.IntList
use array.IntArray
end
theory A
......@@ -19,3 +20,8 @@ theory B
axiom Ax : forall x : t list. true
end
(*
Local Variables:
compile-command: "make -C .. test"
End:
*)
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