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
FinType.eca
(* --------------------------------------------------------------------
* Copyright (c) - 2012-2015 - IMDEA Software Institute and INRIA
* Distributed under the terms of the CeCILL-B licence.
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
require import NewList.
(* -------------------------------------------------------------------- *)
type t.
op elts: t list.
axiom elts_univ x: mem elts x.
axiom elts_uniq : uniq elts.
op cardinality: int = size elts.
Computing file changes ...
