module M1
  use int.Int
  
  goal g: Int.( = ) 4 (Int.( + ) 2 2)
end

module M2
  use int.Int
  
  let f (x : int)
    requires { x = 6 }
    ensures { result = 42 }
  = Int.( * ) x 7
end

module M3
  use int.Int
  use ref.Ref
  
  let f (_ : ())
    ensures { Int.( >= ) result 0 }
  = let x = Ref.ref 42 in Ref.( ! ) x
end

module M4
  use int.Int
  use array.Array
  
  let f (a : Array.array int)
    requires { Int.( >= ) (a.Array.length) 1 }
    writes { a }
    ensures { (Array.( [] ) a 0) = 42 }
  = Array.( []<- ) a 0 42
end
module Mglob
  use int.Int
  
  let ref x = any int
  
  let f (_ : ())
    writes { x [@mlw:reference_var] }
  = (x [@mlw:reference_var]) <- (Int.( + ) x [@mlw:reference_var] 1)
end

module Mscope
  use int.Int
  
  scope S
    function f (x: int) : int = x
    end
  
  import S
  
  goal g: Int.( = ) (2.f) 2
end
module M5
  use int.Int
  use array.Array
  
  let f (a : Array.array int)
    requires { Int.( >= ) (a.Array.length) 1 }
    ensures { (Array.( [] ) a 0) = 42 }
  = Array.( []<- ) a 0 42
end
module M6
  use int.Int
  use array.Array
  
  let f (a : Array.array int)
    requires { Int.( >= ) (a.Array.length) 1 }
    ensures { (Array.( [] ) a 0) = 42 }
  = Array.( []<- ) a 0 42
end
On task 1, alt-ergo answers Valid (<hidden>s, <hidden> steps)
On task 2, alt-ergo answers Valid (<hidden>s, <hidden> steps)
On task 3, alt-ergo answers Valid (<hidden>s, <hidden> steps)
On task 4, alt-ergo answers Valid (<hidden>s, <hidden> steps)
