From 85fd0b333b07c0641c5c9d3a290a2d4d2ead5511 Mon Sep 17 00:00:00 2001 From: Jeehoon Kang Date: Wed, 28 Sep 2022 21:18:34 +0900 Subject: [PATCH] Remove import --- assets/why3/binary_search.mlw | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/assets/why3/binary_search.mlw b/assets/why3/binary_search.mlw index eca628a..2d222bc 100644 --- a/assets/why3/binary_search.mlw +++ b/assets/why3/binary_search.mlw @@ -6,10 +6,10 @@ module BinarySearch - use import int.Int - use import int.ComputerDivision - use import ref.Ref - use import array.Array + use int.Int + use int.ComputerDivision + use ref.Ref + use array.Array let binary_search (a : array int) (v : int) : int requires { forall i1 i2 : int. 0 <= i1 < i2 < length a -> a[i1] <= a[i2] }