Remove import

This commit is contained in:
Jeehoon Kang
2022-09-28 21:18:34 +09:00
parent 5e2a772443
commit 85fd0b333b

View File

@@ -6,10 +6,10 @@
module BinarySearch module BinarySearch
use import int.Int use int.Int
use import int.ComputerDivision use int.ComputerDivision
use import ref.Ref use ref.Ref
use import array.Array use array.Array
let binary_search (a : array int) (v : int) : int let binary_search (a : array int) (v : int) : int
requires { forall i1 i2 : int. 0 <= i1 < i2 < length a -> a[i1] <= a[i2] } requires { forall i1 i2 : int. 0 <= i1 < i2 < length a -> a[i1] <= a[i2] }