Skip to main content

Browse the archive

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 
Replacing Why3 import with manual imports.
 
Some remain in newth/NewIntCore.ec and newth/NewRealCore.ec.
smt full and smt all currently fail for different reasons.
1 parent 966282e
Raw File
StdRing.ec 
(* --------------------------------------------------------------------
 * Copyright (c) - 2012-2015 - IMDEA Software Institute and INRIA
 * Distributed under the terms of the CeCILL-B licence.
 * -------------------------------------------------------------------- *)

(* -------------------------------------------------------------------- *)
require import NewLogic Int Real.
require (*--*) Ring.

(* -------------------------------------------------------------------- *)
axiom invr0: inv 0%r = 0%r.
axiom divr0: forall x, x / 0%r = 0%r.

(* -------------------------------------------------------------------- *)
clone Ring.Field as RField with
  type t <- real,
  op   zeror <- 0%r,
  op   oner  <- 1%r,
  op   ( + ) <- Real.( + ),
  op   [ - ] <- Real.([-]),
  op   ( - ) <- Real.( - ),
  op   ( * ) <- Real.( * ),
  op   ( / ) <- Real.( / ),
  op   invr  <- Real.inv
  proof * by smt.
back to top