Revision 7ae3d64f7211fdb2ca0cfa738fddad52399571fb authored by François Dupressoir on 26 June 2015, 09:46:35 UTC, committed by Pierre-Yves Strub on 26 June 2015, 14:11:43 UTC
Some remain in newth/NewIntCore.ec and newth/NewRealCore.ec. smt full and smt all currently fail for different reasons.
1 parent 966282e
RealSeries.ec
(* --------------------------------------------------------------------
* Copyright (c) - 2012-2015 - IMDEA Software Institute and INRIA
* Distributed under the terms of the CeCILL-B licence.
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
require import Bool Option Fun Distr Int IntExtra Real RealExtra.
require import StdRing StdOrder StdBigop NewList RealSeq.
(*---*) import IterOp BRA.
pragma +implicits.
(* -------------------------------------------------------------------- *)
op partial (s : int -> real) (n : int) : real =
BRA.bigi predT s 0 n.
pred convergeto (s : int -> real) (x : real) =
RealSeq.convergeto (partial s) x.
Computing file changes ...
