dubious_axioms.mlw 446 Bytes
Newer Older
1

2 3
theory Tests

4
  use int.Int
5 6 7 8 9 10 11 12

  axiom a : 1 = 2

  type myRecord = { value : int }

  axiom value_axiom : forall i1 : myRecord. i1.value >= 1

end
13 14 15

theory T

16 17 18 19 20 21 22 23
  type t

  function f t : int

end

theory BadExtension

24
  use int.Int
25

26
  use T
27 28

  axiom a : forall x:t. f x >= 0
29 30

end
31 32 33 34 35

module ProblemWithLemmaFunction

(* this case should not issue a warning *)

36
use int.Int
37 38 39 40 41 42 43

let lemma plus_comm (x y : int) : unit
  ensures { x + y = y + x }
= ()


end