123456789101112131415161718192021222324252627282930313233343536373839404142434445(******************************************************************************)(* *)(* Alt-Ergo: The SMT Solver For Software Verification *)(* Copyright (C) 2013-2018 --- OCamlPro SAS *)(* *)(* This file is distributed under the terms of the license indicated *)(* in the file 'License.OCamlPro'. If 'License.OCamlPro' is not *)(* present, please contact us to clarify licensing. *)(* *)(******************************************************************************)letapplyfl=letres,same=List.fold_left(fun(acc,same)a->letb=fainb::acc,same&&a==b)([],true)lin(ifsamethenlelseList.revres),sameletapply_rightfl=letres,same=List.fold_left(fun(acc,same)(v,a)->letb=fain(v,b)::acc,same&&a==b)([],true)lin(ifsamethenlelseList.revres),sameletrecfind_optpredl=matchlwith|[]->None|e::r->ifpredethenSomeeelsefind_optpredrletto_seql=letrecauxl()=matchlwith|[]->Seq.Nil|x::tail->Seq.Cons(x,auxtail)inauxl