(* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. Inductive mode := | NearestTiesToEven : mode | ToZero : mode | Up : mode | Down : mode | NearestTiesToAway : mode .