Commit 27538456 authored by MARCHE Claude's avatar MARCHE Claude

Realizations of SingleFormat and DoubleFormat

parent 95e8fba7
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import floating_point.GenFloat.
(* Why3 goal *)
Definition double : Type.
exact (t 53 1024).
Defined.
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import floating_point.GenFloat.
(* Why3 goal *)
Definition single : Type.
exact (t 24 128).
Defined.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment