tests/dubious_axioms.mlw

   1
   2 theory Tests
   3
   4   use int.Int
   5
   6   axiom a : 1 = 2
   7
   8   type myRecord = { value : int }
   9
  10   axiom value_axiom : forall i1 : myRecord. i1.value >= 1
  11
  12 end
  13
  14 theory T
  15
  16   type t
  17
  18   function f t : int
  19
  20 end
  21
  22 theory BadExtension
  23
  24   use int.Int
  25
  26   use T
  27
  28   axiom a : forall x:t. f x >= 0
  29
  30 end
  31
  32 module ProblemWithLemmaFunction
  33
  34 (* this case should not issue a warning *)
  35
  36 use int.Int
  37
  38 let lemma plus_comm (x y : int) : unit
  39   ensures { x + y = y + x }
  40 = ()
  41
  42
  43 end